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 |
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 Batty, Brijesh 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 |
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]
|
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 |
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
|