Pre-VaMoS Workshop


We recommend Zoku Hotel Copenhagen (other cheap options are WakeUp and Cabinn)


For information on how to find the university, please refer to this page.

We are in room 3F07. The building is locked for external folks. Please meet at the reception in the main building (as in the link above) at 8.30 am. We will pick you up. If you are late, ask for Andrzej Wasowski (they will contact me, and we will send someone to fetch you).

A word of caution: it is relatively cold in the building. We recommend you bring a spare sweater (just in case).


Monday, January 23, 2023

Let’s meet for dinner in the evening.

We have booked a table at BOB Bistro, Halmtorvet 19, 1700 København V (easily reachable by foot from the main train station) at 7 pm in the name of “ITU Copenhagen”.

Tuesday, January 24, 2023

Coffee and simple bread will be available from 8.30 am in the meeting room.
We expect to finish before 5 pm.

9:00Myra CohenConfigurations Here and There, Configurations Everywhere
9:30Tobias PettCovering T-Wise Feature Interactions Over Time
10:00Mahsa VarshosazStatic Repair of Locking Bugs Using Graph Coloring
10:30Paul BittnerVariability-Aware Source Code Evolution
11:00Thomas ThümTseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses
11:30Lunch Break

13:00Chico SundermannFeature-Model Counting: Obstacles and Advances
13:30Maurice ter BeekCan we Communicate? Using Dynamic Logic to Verify Featured Team Automata
14:00Domenik EichhornThe impact of Quantum Computing on Product Line Analysis
14:30Coffee Break

15:00Sandra GreinerTowards Managing Variability in Space and Time in Heterogeneous Software Artifacts
15:30Adrian HoffUtilizing Software Architecture Recovery to Explore Large-Scale Software Systems in Virtual Reality
16:00Lukas BirkemeyerWhen will we drive autonomously? An investigation from a technical and legal perspective


This event is sponsored by the Independent Research Fund Denmark via the research projects “INSIGHT” and “Immersive Software Archaeology” (0136-00070B)

Talk Abstracts

Covering T-Wise Feature Interactions Over Time – Tobias Pett

Achieving t-wise feature interaction coverage often requires testing many configurations, which is typically infeasible for frequently evolving systems. As testing time is a limiting factor in practice, there has to be a trade-off between testing many configurations of a sample (i.e., high t-wise feature interaction coverage) and reducing testing time. The high testing effort can be mitigated by considering feature interactions covered in previous test executions. However, the current t-wise feature interaction coverage metric does not consider previously tested configurations. In this presentation, we will describe first insights of developing a metric for tracking the ratio of achieved feature interaction coverage over time.

Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses – Thomas Thüm

Feature modeling is widely used to systematically model features of variant-rich software systems and their dependencies. By translating feature models into propositional formulas and analyzing them with solvers, a wide range of automated analyses across all phases of the software development process become possible. Most solvers only accept formulas in conjunctive normal form (CNF), so an additional transformation of feature models is often necessary. However, it is unclear whether this transformation has a noticeable impact on analyses. In this paper, we compare three transformations (i.e., distributive, Tseitin, and Plaisted-Greenbaum) for bringing feature-model formulas into CNF. We analyze which transformation can be used to correctly perform feature-model analyses and evaluate three CNF transformation tools (i.e., FeatureIDE, KConfigReader, and Z3) on a corpus of 22 real-world feature models. Our empirical evaluation illustrates that some CNF transformations do not scale to complex feature models or even lead to wrong results for model-counting analyses. Further, the choice of the CNF transformation can substantially influence the performance of subsequent analyses.

Link to Pre-Print:

Feature-Model Counting: Obstacles and Advances – Chico Sundermann

Managing the complexity of configurable systems and their underlying feature models requires automated support. Many considered analyses depend on feature-model counting, i.e., computing the number of valid configurations, which typically depends on model counting, a computationally complex problem. While existing solutions, such as #SAT solvers, are generally able to evaluate less complex industrial feature models, even state-of-the-art solvers fail for some publicly available feature models. Further, some analyses require thousands of counting computations (e.g., one per feature), demanding scalable solutions, especially for interactive settings. In this talk, we provide an overview on the current state of the art for feature-model counting and discuss ongoing advances. In particular, we provide potential solutions for analyzing very complex feature models and for solving many computations.

Can we Communicate? Using Dynamic Logic to Verify Featured Team Automata – Maurice ter Beek

Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Featured team automata support variability by describing families of concrete product models for specific configurations determined by feature selection. Given a (featured) team automaton one can reason over communication-safety properties, like receptiveness (sent messages must be received) and responsiveness (pending receives must be satisfied), but doing so product-wise quickly becomes impractical. Therefore, we lift these notions to the level of family models and show how to identify such communication properties. However, the purely semantic nature of communication properties is a serious burden in practice, making it challenging to automatically verify such properties in concrete cases: one has to go through all reachable states of networks of interacting automata with large state spaces and check compliance for all requirements at each state. Our solution is to provide the first logical characterisation of communication properties for team automata (and subsumed models) using test-free propositional dynamic logic and, subsequently, to use this characterisation to actually verify communication properties by using available model-checking tools for dynamic logic. An open-source prototypical tool supports the developed theory, using a transformation to interact with the mCRL2 toolset for model checking. Future work concerns generalising our logical characterisation and the tool to deal with variability and family-based compatibility checking for featured team automata.

The impact of Quantum Computing on Product Line Analysis – Domenik Eichhorn

The analysis of product lines is a powerful tool when managing configurable systems. Many analysis techniques are implemented through SAT calls or linear programs, often providing efficient solutions. Still, due to the exponentially growing size of a product line’s configuration space, those methods do not scale for very large systems. Quantum computers can solve such scaling problems by realizing up to polynomial speedups for specific algorithmic problems. In my presentation, I will present the current status of quantum hardware and algorithms and discuss how recent and future progress in the quantum field might impact product line analysis methods.

Towards Managing Variability in Space and Time in Heterogeneous Software Artifacts – Sandra Greiner

Large software systems exhibit high complexity through supporting and evolving different features over time. Thus, these systems vary in space and time. Supported features are, for instance, developed in branches of a version control system (VCS) and merged into the main branch regularly. Research on software product line engineering (SPLE) addresses problems of maintaining both variability dimensions and proposes development techniques, such as feature-oriented programming, the systematic management of annotative software product lines realized through preprocessor directives or variation control systems. While advances in maintaining variable software, such as automatically configuring and testing of variants or ensuring type safety, have been achieved in SPLE, the existing techniques mostly target software specified in C/C++ or Java and mainly require heavy-weight development processes. However, (today’s) software is composed of several heterogeneous artifacts defined in various languages, such as Kotlin or Python, together with, for instance, design models and build scripts. Keeping track of feature realizations between those files is rarely supported in a generic way but is essential to avoid variability bugs and problems caused by forgotten dependencies. The talk explores existing techniques to maintain evolving variability-intensive systems composed of artifacts conforming to different languages. The state-of-the-art either falls short in considering the time dimension or to respect dependencies between different artifacts. Thus, we further sketch a vision of a high-level semantic repsentation for non-product-line repositories which keeps track of related elements in diverse artifacts of one software project potentially spanning multiple branches.

Utilizing Software Architecture Recovery to Explore Large-Scale Software Systems in Virtual Reality – Adrian Hoff

Exploring an unfamiliar large-scale software system is challenging especially when based solely on source code. While software visualizations help in gaining an overview of a system, they generally neglect architecture knowledge in their representations, e.g., by arranging elements along package structures rather than functional components or locking users in a specific abstraction level only slightly above the source code. In this paper, we introduce an automated approach for software architecture recovery and use its results in an immersive 3D virtual reality software visualization to aid accessing and relating architecture knowledge. We further provide a semantic zoom that allows a user to access and relate information both horizontally on the same abstraction level, e.g., by following method calls, and vertically across different abstraction levels, e.g., from a member to its parent class. We evaluate our contribution in a controlled experiment contrasting the usefulness regarding software exploration and comprehension of our concepts with those of the established CityVR visualization and the Eclipse IDE.

When will we drive autonomously? An investigation from a technical and legal perspective – Lukas Birkemeyer

Autonomous driving moves into the focus of society. The German government sees the law on autonomous driving as a milestone that will enable the realization of autonomous driving. Nevertheless, no autonomous driving function that is ready for series production has approval for use on German roads. How far are we from the dream of autonomous driving? In this paper, we examine the unanswered questions that hinder the release of autonomous driving from a legal and technical point of view and point out where both disciplines are waiting for each other. We describe the current status regarding type approval/registration, driver authorization (driver’s license) and liability. In a thought experiment, we replace the human driver with a robot driver; thus, we can compare (advanced) driver assistance systems and automated driving systems. This paper reveals open questions that hinder a proper realization of fully autonomous driving. A practical realization requires close interdisciplinary cooperation between experts in the fields of regulation, technology and social sciences.