ICSE 2024
Fri 12 - Sun 21 April 2024 Lisbon, Portugal

This paper presents Daedalux, a new model-checking platform for variability-intensive systems based on \emph{Featured Transition System} theory developed in C++. Daedalux features a modular, flexible and extensible architecture, overcoming previous tools’ maintainability limitations. In addition, during verification, it provides visualizations of intermediate models and results. A key added value of Daedalux lies in its software architecture, which allows straightforward extension and integration of new formalisms and verification algorithms. We have ourselves implemented two recent FTS-based approaches, i.e. a statistical model checking algorithm for LTL properties and an exhaustive algorithm for multi-LTL properties. By reducing the entry barrier of understanding variability-aware model checking and facilitating the comprehension and extension of the software tools, we hope to increase the ambitions of the community in developing novel model-checking advances. A video demonstration of Daedalux can be found at \url{https://youtu.be/kirpOAlV-0w}.

Wed 17 Apr

Displayed time zone: Lisbon change

14:00 - 15:30
Dependability and Formal methods 1Software Engineering in Practice / Demonstrations / Research Track at Maria Helena Vieira da Silva
Chair(s): Domenico Bianculli University of Luxembourg
14:00
15m
Talk
REDriver: Runtime Enforcement for Autonomous Vehicles
Research Track
Yang Sun Singapore Management University, Chris Poskitt Singapore Management University, Xiaodong Zhang , Jun Sun Singapore Management University
Pre-print
14:15
15m
Talk
Scalable Relational Analysis via Relational Bound Propagation
Research Track
Clay Stevens Iowa State University, Hamid Bagheri University of Nebraska-Lincoln
14:30
15m
Talk
Kind Controllers and Fast Heuristics for Non-Well-Separated GR(1) Specifications
Research Track
Ariel Gorenstein Tel Aviv University, Shahar Maoz Tel Aviv University, Jan Oliver Ringert Bauhaus-University Weimar
14:45
15m
Talk
On the Difficulty of Identifying Incident-Inducing Changes
Software Engineering in Practice
Eileen Kapel ING & Delft University of Technology, Luís Cruz Delft University of Technology, Diomidis Spinellis Athens University of Economics and Business & Delft University of Technology, Arie van Deursen Delft University of Technology
15:00
15m
Talk
Autonomous Monitors for Detecting Failures Early and Reporting Interpretable Alerts in Cloud Operations
Software Engineering in Practice
Adha Hrusto Lund University, Sweden, Per Runeson Lund University, Magnus C Ohlsson System Verification
15:15
7m
Talk
nvshare: Practical GPU Sharing without Memory Size Constraints
Demonstrations
Georgios Alexopoulos University of Athens, Dimitris Mitropoulos University of Athens
Pre-print
15:22
7m
Talk
Daedalux: An Extensible Platform for Variability-Aware Model Checking
Demonstrations
Sami Lazreg Visteon Electronics and Universite Cote d Azur, Maxime Cordy University of Luxembourg, Luxembourg, Simon Thrane Hansen SnT, University of Luxembourg, Axel Legay Université Catholique de Louvain, Belgium
Hide past events