Overall Program

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, Tutorials & Doctoral Symposium Invited talk by Laura Kovacs Invited talk by Harald Rueß Invited talk by Jeannette M. Wing Workshop
09:30 – 10:00
10:00 – 10:30 Contributed Contributed Contributed
10:30 – 11:00 Coffee Break Coffee Break Coffee Break Coffee Break Coffee Break
11:00 – 11:30 Workshop, Tutorials & Doctoral Symposium Contributed Contributed 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, Tutorials & Doctoral Symposium Contributed Contributed Contributed Workshop
14:30 – 15:00
15:00 – 15:30
15:30 – 16:00 Coffee Break Coffee Break Social Event & Dinner Coffee Break Coffee Break
16:00 – 16:30 Workshop, Tutorials & Doctoral Symposium Contributed 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 ACCEPTED PAPERS

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