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
08:45 – 09:00		Opening Session
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		Keynote talk by Laura Kovacs	Keynote talk by Harald Rueß	Keynote talk by Nils Jansen
10:00 – 10:30		Lucas Award	CyberSecurity Presentation by Sebastian Jester	1 Slot a 20 min
10:00 – 10:30		Lucas Award	1 slot a 20 min Contributed	1 Slot a 20 min
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				Luminary Talk by Jeannette M. Wing
15:00 – 15:30				1 slot a 20 min Contributed
15:30 – 16:00	Coffee Break	Coffee Break		Coffee Break	End of the Event
16:00 – 16:30	Workshop, T3, T4 & Doctoral Symposium	4 slots a 20 min Contributed	Social Event & Dinner	4 slots a 20 min Contributed
16:30 – 17:00
17:00 – 17:30
17:30 – 18:00				Closing Session – Announcement of FM24
18:00 – 18:30
18:30 – 19:00
19:00 – 19:30	Reception			PC Dinner

FM DETAILED PROGRAM

FM-Program-1 Herunterladen

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

Proceedings

The Proceedings for FM23 are available here. Please use only the below provided links to made the access and its autentification working:

https://link.springer.com/book/10.1007/978-3-031-27481-7

This year we celebrate the 25th edition of FM!
Springer is celebrating with us and made the proceedings of the previous editions freely accessible:

https://link.springer.com/book/10.1007/978-3-031-27481-7

https://link.springer.com/book/10.1007/978-3-030-90870-6

https://link.springer.com/book/10.1007/978-3-030-54994-7

https://link.springer.com/book/10.1007/978-3-030-54997-8

https://link.springer.com/book/10.1007/978-3-030-30942-8

https://link.springer.com/book/10.1007/978-3-319-95582-7

https://link.springer.com/book/10.1007/978-3-319-48989-6

https://link.springer.com/book/10.1007/978-3-319-19249-9

https://link.springer.com/book/10.1007/978-3-319-06410-9