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, 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


PaperAuthors
The Octatope Abstract Domain for Verification of Neural NetworksTaylor Dohmen, Stanley BakAshutosh Trivedi, Alvaro Velasquez, Piotr Wojciechowski and K. Subramani
The ScalaFix equation solverGianluca Amato and Francesca Scozzari
Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B RefinementTsutomu Kobayashi, Martin Bondu and Fuyuki Ishikawa
Energy Problems in Finite and Timed Automata with Büchi ConditionsSven Dziadek, Uli Fahrenberg and Philipp Schlehuber-Caissier
SMT Sampling via Model-Guided ApproximationMatan PeledBat-Chen Rothenberg and Shachar Itzhaky
Minimisation of Spatial Models using Branching BisimilarityVincenzo Ciancia, Jan Friso Groote, Diego LatellaMieke Massink and Erik De Vink
Efficient SMT-based Network Fault Tolerance VerificationYu Liu, Pavle Subotic, Emmanuel Letier, Sergey Mechtaev and Abhik Roychoudhury
A Coq formalization of Lebesgue Induction Principle and Tonelli’s TheoremSylvie BoldoFrancois Clement, Vincent Martin, Micaela Mayero and Houda Mouhcine
Abstract Alloy InstancesJan Oliver Ringert and Allison K. Sullivan
QMaude: quantitative specification and verification in rewriting logicRubén Rubio, Narciso Marti-Oliet, Isabel Pita and Alberto Verdejo
Monitoring the Internet ComputerDavid 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 ProgramsFortunat Rajaona, Ioana Boureanu, Vadim Malvone and Francesco Belardinelli
Verifying Feedforward Neural Networks for Classification in Isabelle/HOLAchim D. Brucker and Amy Stell
PFL: a Probabilistic Logic for Fault TreesStefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, E. Moritz Hahn and Mariëlle Stoelinga
Can we Communicate? Using Dynamic Logic to Verify Team AutomataMaurice H. ter Beek, Guillermina Cledou, Rolf Hennicker and José Proença
symQV: Automated Symbolic Verification of Quantum ProgramsFabian Bauer-Marquart, Stefan Leue and Christian Schilling
Reasoning about Promises in Weak Memory Models with Event StructuresHeike Wehrheim, Lara Bargmann and Brijesh Dongol
SMPT: A Testbed for Reachabilty Methods in Generalized Petri NetsNicolas Amat and Silvano Dal Zilio
Formalising the Prevention of Microarchitectural Timing Channels by Operating SystemsRobert Sison, Scott Buckley, Toby Murray, Gerwin Klein and Gernot Heiser
A Decision Diagram Operation for ReachabilitySebastiaan Brand, Thomas Bäck and Alfons Laarman
A fine-grained semantics for arrays and pointers under weak memory modelsRobert Colvin
VeyMont: Parallelising Verified Programs instead of Verifying Parallel ProgramsPetra van den Bos and Sung-Shik Jongmans
Verifying At the Level of Java BytecodeMarco Paganoni and Carlo A. Furia
A Runtime Environment for Contract AutomataDavide Basile and Maurice H. ter Beek
Tableaux for Realizability of Safety SpecficationsMontserrat Hermo, Paqui Lucio and Cesar Sanchez
HHLPy: Practical Verification of Hybrid Systems using Hoare LogicHuanhuan Sheng, Alexander Bentkamp and Bohua Zhan
Word Equations in Synergy with Regular ConstraintsFrantišek Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš HolíkOndrej Lengal and Juraj Síč
Railway Scheduling Using Boolean Satisfiability Modulo SimulationsTomáš Kolárik and Stefan Ratschan