Nov. 22 22:00-02:00
Nov. 23 22:00-02:20
Nov. 24 22:00-02:20
Nov. 25 22:00-00:40
Nov. 26 20:00-02:40
Beijing Time, UTC +8:00
Monday, November 22nd
22:00
OPENING [Video]
22:20-23:00Session 1: Interactive Theorem Proving
Chair:
Marieke Huisman
22:20
Verifying Secure Speculation in Isabelle/HOL [Video]
Presenter: Matt Griffin
22:40
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin and Philippa Gardner
Two mechanisations of WebAssembly 1.0 [Video]
Presenter: Conrad Watt
23:00-23:20Break
23:20-00:40Session 2: Neural Networks & Active Learning
Chair:
Nils Jansen
23:20
Bing Sun, Jun Sun, Ting Dai and Lijun Zhang
Probabilistic Verification of Neural Networks Against Group Fairness [Video]
Presenter: Bing Sun
23: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
00:00
Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers [Video]
Presenter: Stefan Mitsch, Aleksey Nogin
00: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
00:40-01:00Break
01:00-02:00Session 3
Chair:
Corina Pasareanu
01:00
Clark Barrett (joint with MEMOCODE)
Domain-Specific Reasoning with Satisfiability Modulo Theories (Invited Talk) [Video]
Tuesday, November 23rd
22:00-23:00Session 4
Chair:
Marieke Huisman
22:00
Paula Herber
Combine Forces - How to Formally Verify Informally Defined Embedded Systems (Invited Talk) [Video]
23:00-23:20Break
23:20-00:40Session 5: Logics & Theory
Chair:
Paula Herber
23:20
Gal Amram, Shahar Maoz, Or Pistiner and Jan Oliver Ringert
Efficient Algorithms for ω-Regular Energy Games [Video]
23:40
Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers [Video]
Presenter: Khushraj Madnani
00:00
Matias Scharager, Katherine Cordwell, Stefan Mitsch and André Platzer
Verified Quadratic Virtual Substitution for Real Arithmetic [Video]
Presenter: Matias Scharager
00:20
Rim Saddem-Yagoubi, Pascal Poizat and Sara Houhou
Business Processes Meet Spatial Concerns: the sBPMN Verification Framework [Video]
00:40-01:00Break
01:00-02:20Session 6: Program Verification Ⅰ
Chair:
Anton Wijs
01:00
Mark BattyBrijesh Dongol and Daniel Wright
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies [Video]
01: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]
01:40
Alexandra Bugariu, Arshavir Ter-Gabrielyan and Peter Müller
Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers [Video]
02:00
Nicholas Coughlin, Kirsten Winter and Graeme Smith
Rely/guarantee reasoning for multicopy atomic weak memory models [Video]
Presenter: Nicholas Coughlin
Wednesday, November 24th
22:00-23:00Session 7
Chair:
Ana Cavalcanti
22:00
FME Fellow [Video]
23:00-23:20Break
23:20-00:40Session 8: Hybrid Systems
Chair:
Tarmo Uustalu
23: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
23:40
Zhenya Zhang and Paolo Arcaini
Gaussian Process-Based Confidence Estimation for Hybrid System Falsification [Video]
Presenter: Zhenya Zhang
00:00
Formal Verification of Intelligent Hybrid Systems that are modeled with Simulink and the Reinforcement Learning Toolbox [Video]
00: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
00:40-01:00Break
01:00-02:20Session 9: Program Verification Ⅱ
Chair:
Dorel Lucanu
01:00
Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka and Vijay Ganesh
Z3str4: A Multi-armed String Solver [Video]
01: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
01:40
Adel Djoudi, Martin Hana and Nikolai Kosmatov
Formal verification of a JavaCard virtual machine with Frama-C [Video]
02:00
Verification of the Incremental Merkle Tree Algorithm with Dafny [Video]
Thursday, November 25th
22:00-23:00Session 10
Chair:
Stefania Gnesi
22:00
Assia Mahboubi
Formal verification of computational mathematics (Invited Talk) [Video]
23:00-23:20Break
23:20-00:40Session 11: Automata
Chair:
Radu Mateescu
23:20
Congruence Relations for Büchi Automata [Video]
23:40
Featured Team Automata [Video]
Presenter: Guillermina Cledou
00: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]
00:20
Andrea Pferscher and Bernhard K. Aichernig
Fingerprinting Bluetooth Low Energy Devices via Active Automata Learning
Presenter: Andrea Pferscher [Video]
Friday, November 26th
20:00-21:00Session 12
Chair:
Naijun Zhan
20:00
Mingsheng Ying
Model Checking for Verification of Quantum Circuits (Invited Talk) [Video]
21:00-21:20Break
21:20-23:00Session 13: Journal First Track
Chair:
Eerke Boiten
21:20
Rob Hierons
FSM quasi-equivalence testing via reduction and observing absences [Video]
21:40
Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fishe
Multi-scale verification of distributed synchronisation [Video]
22:00
Marcello M. Bersani, Matteo Soldo, Claudio Menghi, Patrizio Pelliccione & Matteo Rossi
PuRSUE -from specification of robotic environments to synthesis of controllers [Video]
22:20
Gavin Lowe
Discovering and correcting a deadlock in a channel implementation [Video]
22:40
Marco Bozzano, Alessandro Cimatti,Cristian Mattarei
Formal reliability analysis of redundancy architectures [Video]
23:00-23:20Break
23:20-00:40Session 14: Analysis of Complex Systems
Chair:
Rosemary Monahan
23:20
Weijiang Hong, Zhenbang Chen, Yide Du and Ji Wang
Trace Abstraction-based Verification for Uninterpreted Programs [Video]
23:40
Felipe Gorostiaga and Cesar Sanchez
HStriver: a Very Functional Extensible Tool for the Runtime Verification of Real-Time Event Streams [Video]
Presenter: Felipe Gorostiaga
00:00
Cui Su and Jun Pang
CABEAN 2.0: Efficient and Efficacious Control of Asynchronous Boolean Networks [Video]
00:20
Ionut Tutu, Claudia Chirita and José Luiz Fiadeiro
Dynamic Reconfiguration via Typed Modalities [Video]
00:40-01:00Break
01:00-02:40Session 15: Probabilities
Chair:
Maurice ter Beek
01: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ć
01: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
01:40
HyperProb: A Model Checker for Probabilistic Hyperproperties (short) [Video]
01:50
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen and Laura Kovács
The Probabilistic Termination Tool Amber (short) [Video]
02:00
Rong Gu, Cristina Seceleanu, Eduard Enoiu and Kristina Lundqvist
Model Checking Collision Avoidance of Nonlinear Autonomous Vehicle Models [Video]
Presenter: Rong Gu
02:20
Closing of Conference [Video]
1. Presentation of Best Paper Award
2. Announcement on FM 2023