Programs for Co-Located Events
The three co-located events have their own programs:
- Formal Ethical Agents and Robots (FEAR) (11 Nov)
- Formal Methods for Autonomous Systems (FMAS) (11–13 Nov)
- PhD Symposium (12 Nov)
Note that iFM and FMAS share the morning session 09:20–12:35 on Wednesday, 13 Nov.
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.
Proof for Industrial Systems using Neural Certificates
Daniel Kröning
Daniel Kröning
10:30–11:00
Coffee Break
11:00–12:30
iFM Practices and Verification. Shared iFM/FMAS session. Session Chair: Mengwei Xu.
A Formal Tainting-Based Framework for Malware Analysis
Andrei-Catalin Mogage and Dorel Lucanu
Andrei-Catalin Mogage and Dorel Lucanu
Formalizing Stateful Behavior Trees
Serena Serbinowska, Preston Robinette, Gabor Karsai, and Taylor T Johnson
Serena Serbinowska, Preston Robinette, Gabor Karsai, and Taylor T Johnson
A Systematic Literature Review on a Decade of Industrial TLA+ Practice (short paper)
Roman Bögli, Leandro Lerena, Christos Tsigkanos and Timo Kehrer
Roman Bögli, Leandro Lerena, Christos Tsigkanos and Timo Kehrer
Proving Termination via Measure Transfer in Equivalence Checking (short paper)
Dragana Milovančević, Carsten Fuhs, Mario Bucev and Viktor Kunčak
Dragana Milovančević, Carsten Fuhs, Mario Bucev and Viktor Kunčak
12:30–12:35
FMAS Closing Remarks
12:35–14:00
Lunch (South Gallery)
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
Logan Murphy, Torin Viger, Alessio Di Sandro and Marsha Chechik
Stateful Functional Modeling with Refinement (A Lean4 Framework)
Frederic Peschanski
Frederic Peschanski
Modeling Register Pairs in CompCert
Alexander Loitzl and Florian Zuleger
Alexander Loitzl and Florian Zuleger
18:00
Welcome Reception
Thursday, 14 Nov 2024
09:30–10:30
Software Verification. Session Chair: Carlo A. Furia.
Implementing, Specifying, and Verifying the QOI Format in Dafny: A Case Study
Stefan Ciobaca and Diana-Elena Gratie
Stefan Ciobaca and Diana-Elena Gratie
VeriCode: Correct Translation of Abstract Specifications to C Code
Gerhard Schellhorn, Stefan Bodenmüller and Wolfgang Reif
Gerhard Schellhorn, Stefan Bodenmüller and Wolfgang Reif
10:30–11:00
Coffee Break
11:00–12:30
Quantitative Analysis and Monitoring. Session Chair: Clare Dixon.
Monitoring Extended Hypernode Logic
Marek Chalupa, Thomas Henzinger and Ana Oliveira da Costa
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
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
Martin Fränzle, Thomas Møller Grosen, Kim Guldstrand Larsen and Martin Zimmermann
12:30–14:00
Lunch and Poster/Demo Session (South Gallery)
14:00–15:30
Invited Tutorial. Session Chair: Mohammad Reza Mousavi.
Deductive Verification of C Programs with Frama-C
Frédéric Loulergue
Frédéric Loulergue
15:30–16:30
Coffee Break and Poster/Demo Session (South Gallery)
17:00
Social Event and Conference Dinner
Friday, 15 Nov 2024
09:30–10:30
Keynote talk. Session Chair: Marie Farrell.
A Formal Approach to Railways Interlocking Design
Alessandro Cimatti
Alessandro Cimatti
10:30–11:00
Coffee Break
11:00–12:30
System Analysis and Security. Session Chair: Conor Reynolds.
VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory
Robert Rubbens, Petra van den Bos and Marieke Huisman
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
Erik Voogd, Einar Broch Johnsen, Åsmund Aqissiaq Arild Kløvstad, Jurriaan Rot and Alexandra Silva
Solvent: Liquidity Verification of Smart Contracts (short paper)
Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini and Vadim Malvone
Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini and Vadim Malvone
STEVE: A Rational Verification Tool for Stackelberg Security Games (short paper)
Surasak Phetmanee, Michele Sevegnani and Oana Andrei
Surasak Phetmanee, Michele Sevegnani and Oana Andrei
12:30–14:00
Lunch (South Gallery)
14:00–15:30
Learning and Reasoning. Session Chair: Rosemary Monahan.
PyQBF: A Python Framework for Solving Quantified Boolean Formulas (short paper)
Mark Peyrer, Maximilian Heisinger and Martina Seidl
Mark Peyrer, Maximilian Heisinger and Martina Seidl
Active Learning of Runtime Monitors Under Uncertainty (short paper)
Sebastian Junges, Sanjit A. Seshia and Hazem Torfah
Sebastian Junges, Sanjit A. Seshia and Hazem Torfah
Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods
George Granberry, Wolfgang Ahrendt and Moa Johansson
George Granberry, Wolfgang Ahrendt and Moa Johansson
Improving SAT Solver Performance through MLP-Predicted Genetic Algorithm Parameters (short paper)
Sabrine Saouli, Souheib Baarir and Claude Dutheillet
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).
The duration of a short paper presentation is 10 min (+ 5 min Q&A).
