Wednesday, 13 Nov 2024

08:45–09:20
Arrival and Registration
09:20–09:30
Opening. Nikolai Kosmatov, Laura Kovács (PC Chairs), Marie Farrell, Mohammad Reza Mousavi (General Chairs).
09:30–10:30
Shared iFM/FMAS Keynote. Session chair: Laura Kovács.
10:30–11:00
Coffee Break
11:00–12:30
iFM Practices and Verification. Shared iFM/FMAS session. Session chair: TBD.
A Formal Tainting-Based Framework for Malware Analysis
Andrei-Catalin Mogage and Dorel Lucanu
TBD (An FMAS Paper)
A Systematic Literature Review on a Decade of Industrial TLA+ Practice
Roman Bögli, Leandro Lerena, Christos Tsigkanos and Timo Kehrer
Proving Termination via Measure Transfer in Equivalence Checking
Dragana Milovančević, Carsten Fuhs, Mario Bucev and Viktor Kunčak
12:30–14:00
Lunch
14:00–15:00
Keynote talk. Session Chair: Nikolai Kosmatov.
15:00–15:30
Coffee Break
15:30–17:00
Verification and Refinement. Best Paper Award Candidates. Session chair: Wolfgang Ahrendt.
PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases
Logan Murphy, Torin Viger, Alessio Di Sandro and Marsha Chechik
Stateful Functional Modeling with Refinement (A Lean4 Framework)
Frederic Peschanski
Modeling Register Pairs in CompCert
Alexander Loitzl and Florian Zuleger
18:00
Welcome Reception

Thursday, 14 Nov 2024

09:30–10:30
Software Verification. Session Chair: TBD.
Implementing, Specifying, and Verifying the QOI Format in Dafny: A Case Study
Stefan Ciobaca and Diana-Elena Gratie
VeriCode: Correct Translation of Abstract Specifications to C Code
Gerhard Schellhorn, Stefan Bodenmüller and Wolfgang Reif
10:30–11:00
Coffee Break
11:00–12:30
Quantitative Analysis and Monitoring. Session chair: TBD.
Monitoring Extended Hypernode Logic
Marek Chalupa, Thomas Henzinger and Ana Oliveira da Costa
Towards Quantitative Analysis of Simulink Models using Stochastic Hybrid Automata
Pauline Blohm, Paula Herber and Anne Remke
Monitoring Real-Time Systems under Parametric Delay
Martin Fränzle, Thomas Møller Grosen, Kim Guldstrand Larsen and Martin Zimmermann
12:30–14:00
Lunch and Poster/Demo Session
14:00–15:30
Invited Tutorial. Session Chair: Mohammad Reza Mousavi.
The Frama-C Software Verification Platform
Frédéric Loulergue
15:30–16:30
Coffee Break and Poster/Demo Session
17:00
Social Event and Conference Dinner

Friday, 15 Nov 2024

09:30–10:30
Keynote talk. Session Chair: Marie Farrell.
10:30–11:30
Coffee Break
11:00–12:30
System Analysis and Security. Session chair: TBD.
VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory
Robert Rubbens, Petra van den Bos and Marieke Huisman
Correct and Complete Symbolic Execution for Free
Erik Voogd, Einar Broch Johnsen, Åsmund Aqissiaq Arild Kløvstad, Jurriaan Rot and Alexandra Silva
Solvent: Liquidity Verification of Smart Contracts
Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini and Vadim Malvone
STEVE: A Rational Verification Tool for Stackelberg Security Games
Surasak Phetmanee, Michele Sevegnani and Oana Andrei
12:30–14:00
Lunch
14:00–15:30
Learning and Reasoning. Session Chair: TBD.
PyQBF: A Python Framework for Solving Quantified Boolean Formulas
Mark Peyrer, Maximilian Heisinger and Martina Seidl
Active Learning of Runtime Monitors Under Uncertainty
Sebastian Junges, Sanjit A. Seshia and Hazem Torfah
Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods
George Granberry, Wolfgang Ahrendt and Moa Johansson
Improving SAT Solver Performance through MLP-Predicted Genetic Algorithm Parameters
Sabrine Saouli, Souheib Baarir and Claude Dutheillet
15:30–15:40
Closing. Nikolai Kosmatov, Laura Kovács (PC Chairs), Marie Farrell, Mohammad Reza Mousavi (General Chairs).
15:40–16:00
Coffee Break
16:00
End of the Conference
The duration of a regular paper presentation is 25 min (+ 5 min Q&A).
The duration of a short paper presentation is 10 min (+ 5 min Q&A).