Nov. 22 06:00-10:00
Nov. 23 06:00-10:20
Nov. 24 06:00-10:20
Nov.25 06:00-08:40
Nov. 26 04:00-10:20
San Francisco Time, UTC -8:00
Monday, November 22nd
06:00
OPENING [Video]
06:20-07:00Session 1: Interactive Theorem Proving
Chair:
Marieke Huisman
06:20
Verifying Secure Speculation in Isabelle/HOL [Video]
Presenter: Matt Griffin
06:40
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin and Philippa Gardner
Two mechanisations of WebAssembly 1.0 [Video]
Presenter: Conrad Watt
07:00-07:20Break
07:20-08:40Session 2: Neural Networks & Active Learning
Chair:
Nils Jansen
07:20
Bing Sun, Jun Sun, Ting Dai and Lijun Zhang
Probabilistic Verification of Neural Networks Against Group Fairnes [Video]
Presenter:Bing Sun
07:40
Joseph Scott, Hammad Rehman, Trishal Sudula, Federico Mora and Vijay Ganesh
BanditFuzz: Fuzzing SMT Solvers with Multi-Agent Reinforcement Learning [Video]
Presenter: Federico Mora
08:00
Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers [Video]
Presenter: Stefan Mitsch, Aleksey Nogin
08:20
Ernst Moritz Hahn, Mateo Perez, Sven ScheweFabio SomenziAshutosh Trivedi and Dominik Wojtczak
Model-Free Reinforcement Learning for Lexicographic Omega-Regular Objectives [Video]
Presenter: Mateo Perez
08:40-09:00Break
09:00-10:00Session 3
Chair:
Corina Pasareanu
09:00
Clark Barrett (joint with MEMOCODE)
Domain-Specific Reasoning with Satisfiability Modulo Theories (Invited Talk) [Video]
Tuesday, November 23rd
06:00-07:00Session 4
Chair:
Marieke Huisman
06:00
Paula Herber
Combine Forces - How to Formally Verify Informally Defined Embedded Systems (Invited Talk) [Video]
07:00-07:20Break
07:20-08:40Session 5: Logics & Theory
Chair:
Paula Herber
07:20
Gal Amram, Shahar Maoz, Or Pistiner and Jan Oliver Ringert
Efficient Algorithms for ω-Regular Energy Games [Video]
07:40
Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers [Video]
Presenter:  Khushraj Madnani
08:00
Matias Scharager, Katherine Cordwell, Stefan Mitsch and André Platzer
Verified Quadratic Virtual Substitution for Real Arithmetic [Video]
Presenter: Matias Scharager
08:20
Rim Saddem-Yagoubi, Pascal Poizat and Sara Houhou
Business Processes Meet Spatial Concerns: the sBPMN Verification Framework [Video]
08:40-09:00Break
09:00-10:20Session 6: Program Verification Ⅰ
Chair:
Anton Wijs
09:00
Mark BattyBrijesh Dongol and Daniel Wright
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies [Video]
09:20
Jinting Bian, Hans-Dieter Hiep, Frank De Boer and Stijn De Gouw
Integrating ADTs in KeY and their Application to History-based Reasoning [Video]
09:40
Alexandra Bugariu, Arshavir Ter-Gabrielyan and Peter Müller
Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers [Video]
10:00
Nicholas Coughlin, Kirsten Winter and Graeme Smith
Rely/guarantee reasoning for multicopy atomic weak memory models [Video]
Presenter: Nicholas Coughlin
Wednesday, November 24th
06:00-07:00Session 7
Chair:
Ana Cavalcanti
07:00
FME Fellow [Video]
07:00-07:20Break
07:20-08:40Session 8: Hybrid Systems
Chair:
Tarmo Uustalu
07:20
Sota Sato, Atsuyoshi SaimenMasaki Waga, Kenji Takao and Ichiro Hasuo
Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: a Gas Turbine Case Study [Video]
Presenter: Atsuyoshi Saimen
07:40
Zhenya Zhang and Paolo Arcaini
Gaussian Process-Based Confidence Estimation for Hybrid System Falsification [Video]
Presenter: Zhenya Zhang
08:00
Formal Verification of Intelligent Hybrid Systems that are modeled with Simulink and the Reinforcement Learning Toolbox [Video]
08:20
Simon Foster, Mario Gleirscher, Jonathan Huerta Y Munive and Georg Struth
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs [Video]
Presenter: Jonathan Huerta Y Munive
08:40-09:00Break
09:00-10:20Session 9: Program Verification Ⅱ
Chair:
Dorel Lucanu
09:00
Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka and Vijay Ganesh
Z3str4: A Multi-armed String Solver [Video]
09:20
Felix A. Wolf, Malte Schwerhoff and Peter Müller
Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA [Video]
Presenter: Felix A. Wolf
09:40
Adel Djoudi, Martin Hana and Nikolai Kosmatov
Formal verification of a JavaCard virtual machine with Frama-C [Video]
10:00
Verification of the Incremental Merkle Tree Algorithm with Dafny [Video]
Thursday, November 25th
06:00-07:00Session 10
Chair:
Stefania Gnesi
07:00
Assia Mahboubi
Formal verification of computational mathematics (Invited Talk) [Video]
07:00-07:20Break
07:20-08:40Session 11: Automata
Chair:
Radu Mateescu
07:20
Congruence Relations for Büchi Automata [Video]
07:40
Featured Team Automata [Video]
Presenter: Guillermina Cledou
08:00
Anastasia Mavridou, Andreas Katis, Dimitra Giannakopoulou, David Kooi, Thomas Pressburger and Michael W. Whalen
From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET [Video]
08:20
Andrea Pferscher and Bernhard K. Aichernig
Fingerprinting Bluetooth Low Energy Devices via Active Automata Learning [Video]
Presenter: Andrea Pferscher
Friday, November 26th
04:00-05:00Session 12
Chair:
Naijun Zhan
04:00
Mingsheng Ying
Model Checking for Verification of Quantum Circuits (Invited Talk) [Video]
05:00-05:20Break
05:20-07:00Session 13: Journal First Track
Chair:
Eerke Boiten
05:20
Rob Hierons
FSM quasi-equivalence testing via reduction and observing absences [Video]
05:40
Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fishe
Multi-scale verification of distributed synchronisation [Video]
06:00
Marcello M. Bersani, Matteo Soldo, Claudio Menghi, Patrizio Pelliccione & Matteo Rossi
PuRSUE -from specification of robotic environments to synthesis of controllers [Video]
06:20
Gavin Lowe
Discovering and correcting a deadlock in a channel implementation [Video]
06:40
Marco Bozzano, Alessandro Cimatti,Cristian Mattarei
Formal reliability analysis of redundancy architectures [Video]
07:00-07:20Break
07:20-08:40Session 14: Analysis of Complex Systems
Chair:
Rosemary Monahan
07:20
Weijiang Hong, Zhenbang Chen, Yide Du and Ji Wang
Trace Abstraction-based Verification for Uninterpreted Programs [Video]
07:40
Felipe Gorostiaga and Cesar Sanchez
HStriver: a Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams [Video]
Presenter: Felipe Gorostiage
08:00
Cui Su and Jun Pang
CABEAN 2.0: Efficient and Efficacious Control of Asynchronous Boolean Networks [Video]
08:20
Ionut Tutu, Claudia Chirita and José Luiz Fiadeiro
Dynamic Reconfiguration via Typed Modalities [Video]
08:40-09:00Break
09:00-10:40Session 15: Probabilities
Chair:
Maurice ter Beek
09:00
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky and Đorđe Žikelić
On Lexicographic Proof Rules for Probabilistic Termination [Video]
Presenter: Đorđe Žikelić
09:20
František Blahoudek, Murat CubuktepePetr NovotnýMelkior OrnikPranay Thangeda and Ufuk Topcu
Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption [Video]
Presenter: Pranay Thangeda
09:40
HyperProb: A Model Checker for Probabilistic Hyperproperties (short) [Video]
09:50
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen and Laura Kovács
The Probabilistic Termination Tool Amber (short) [Video]
10:00
Rong Gu, Cristina Seceleanu, Eduard Enoiu and Kristina Lundqvist
Model Checking Collision Avoidance of Nonlinear Autonomous Vehicle Models [Video]
Presenter: Rong Gu
10:20  Closing of Conference [Video]
1. Presentation of Best Paper Award
2. Announcement on FM 2023