SCHEDULE
| Monday March, 6th |
Tuesday, March, 7th |
Wednesday March, 8th |
Thursday March, 9th |
Friday March, 10th |
|
|---|---|---|---|---|---|
| Workshop, Tutorials & Doctoral Symposium | Main FM Conference | Workshop | |||
| Industry Day | D-CON 2023 | D-CON 2023 | |||
| Time | Monday March, 6th |
Tuesday, March, 7th |
Wednesday March, 8th |
Thursday March, 9th |
Friday March, 10th |
| 09:00 – 09:30 | Workshop, T1, T2, T4 & Doctoral Symposium | Keynote talk by Laura Kovacs | Keynote talk by Harald Rueß | Keynote talk by Nils Jansen | Workshop |
| 09:30 – 10:00 | |||||
| 10:00 – 10:30 | Lucas Award | CyberSecurity Presentation | 1 Slot a 20 min | ||
| 1 slot a 20 min Contributed | |||||
| 10:30 – 11:00 | Coffee Break | Coffee Break | Coffee Break | Coffee Break | Coffee Break |
| 11:00 – 11:30 | Workshop, T1, T2, T4 & Doctoral Symposium | 4 slots a 20 min Contributed | 4 slots a 20 min Contributed | 4 slots a 20 min Contributed | Workshop |
| 11:30 – 12:00 | |||||
| 12:00 – 12:30 | |||||
| 12:30 – 13:00 | Lunch | Lunch | Lunch | Lunch | Lunch |
| 13:00 – 13:30 | |||||
| 13:30 – 14:00 | |||||
| 14:00 – 14:30 | Workshop, T3, T4 & Doctoral Symposium | 4 slots a 20 min Contributed | 5 slots a 20 min Contributed | Luminary Talk by Jeannette M. Wing | Workshop |
| 14:30 – 15:00 | |||||
| 15:00 – 15:30 | 1 slot a 20 min Contributed | ||||
| 15:30 – 16:00 | Coffee Break | Coffee Break | Coffee Break | Coffee Break | |
| 16:00 – 16:30 | Workshop, T3, T4 & Doctoral Symposium | 4 slots a 20 min Contributed | Social Event & Dinner | 4 slots a 20 min Contributed | Workshop |
| 16:30 – 17:00 | |||||
| 17:00 – 17:30 | |||||
| 17:30 – 18:00 | End of the Event | ||||
| 18:00 – 18:30 | Reception | ||||
| 18:30 – 19:00 | |||||
| 19:00 – 19:30 | PC Dinner | ||||
FM DETAILED PROGRAM
FM ACCEPTED PAPERS
| Paper | Authors |
| The Octatope Abstract Domain for Verification of Neural Networks | Taylor Dohmen, Stanley Bak, Ashutosh Trivedi, Alvaro Velasquez, Piotr Wojciechowski and K. Subramani |
| The ScalaFix equation solver | Gianluca Amato and Francesca Scozzari |
| Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement | Tsutomu Kobayashi, Martin Bondu and Fuyuki Ishikawa |
| Energy Problems in Finite and Timed Automata with Büchi Conditions | Sven Dziadek, Uli Fahrenberg and Philipp Schlehuber-Caissier |
| SMT Sampling via Model-Guided Approximation | Matan Peled, Bat-Chen Rothenberg and Shachar Itzhaky |
| Minimisation of Spatial Models using Branching Bisimilarity | Vincenzo Ciancia, Jan Friso Groote, Diego Latella, Mieke Massink and Erik De Vink |
| Efficient SMT-based Network Fault Tolerance Verification | Yu Liu, Pavle Subotic, Emmanuel Letier, Sergey Mechtaev and Abhik Roychoudhury |
| A Coq formalization of Lebesgue Induction Principle and Tonelli’s Theorem | Sylvie Boldo, Francois Clement, Vincent Martin, Micaela Mayero and Houda Mouhcine |
| Abstract Alloy Instances | Jan Oliver Ringert and Allison K. Sullivan |
| QMaude: quantitative specification and verification in rewriting logic | Rubén Rubio, Narciso Marti-Oliet, Isabel Pita and Alberto Verdejo |
| Monitoring the Internet Computer | David Basin, Daniel Stefan Dietiker, Srdjan Krstic, Yvonne-Anne Pignolet, Martin Raszyk, Joshua Schneider and Arshavir Ter-Gabrielyan |
| Program Semantics and Verification Technique for AI-centred Programs | Fortunat Rajaona, Ioana Boureanu, Vadim Malvone and Francesco Belardinelli |
| Verifying Feedforward Neural Networks for Classification in Isabelle/HOL | Achim D. Brucker and Amy Stell |
| PFL: a Probabilistic Logic for Fault Trees | Stefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, E. Moritz Hahn and Mariëlle Stoelinga |
| Can we Communicate? Using Dynamic Logic to Verify Team Automata | Maurice H. ter Beek, Guillermina Cledou, Rolf Hennicker and José Proença |
| symQV: Automated Symbolic Verification of Quantum Programs | Fabian Bauer-Marquart, Stefan Leue and Christian Schilling |
| Reasoning about Promises in Weak Memory Models with Event Structures | Heike Wehrheim, Lara Bargmann and Brijesh Dongol |
| SMPT: A Testbed for Reachabilty Methods in Generalized Petri Nets | Nicolas Amat and Silvano Dal Zilio |
| Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems | Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein and Gernot Heiser |
| A Decision Diagram Operation for Reachability | Sebastiaan Brand, Thomas Bäck and Alfons Laarman |
| A fine-grained semantics for arrays and pointers under weak memory models | Robert Colvin |
| VeyMont: Parallelising Verified Programs instead of Verifying Parallel Programs | Petra van den Bos and Sung-Shik Jongmans |
| Verifying At the Level of Java Bytecode | Marco Paganoni and Carlo A. Furia |
| A Runtime Environment for Contract Automata | Davide Basile and Maurice H. ter Beek |
| Tableaux for Realizability of Safety Specfications | Montserrat Hermo, Paqui Lucio and Cesar Sanchez |
| HHLPy: Practical Verification of Hybrid Systems using Hoare Logic | Huanhuan Sheng, Alexander Bentkamp and Bohua Zhan |
| Word Equations in Synergy with Regular Constraints | František Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondrej Lengal and Juraj Síč |
| Railway Scheduling Using Boolean Satisfiability Modulo Simulations | Tomáš Kolárik and Stefan Ratschan |