Schedule
Day 1 - May 05, 2026
Session 1: Keynote Session (Chair: Klaus Havelund)
| 09:00 - 10:00 |
Tudor Achim
Mathematical Superintelligence: From Competition Mathematics to Formal Verification
|
| 10:00 - 10:30 |
Coffee Break
|
Session 2: Distributed Systems & Solver Verification (Chair: Anastasia Mavridou)
| 10:30 - 11:00 |
Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition
William Schultz, Edward Ashton, Heidi Howard, Stavros Tripakis
|
| 11:00 - 11:30 |
DisQ: A Model of Distributed Quantum Processors
Le Chang, Saitej Yavvari, W. Rance Cleaveland, Samik Basu, Runzhou Tao, Liyi Li
|
| 11:30 - 12:00 |
Verifying a Solver for Mixed Flow-Sensitive Analyses
Sarah Tilscher, Alexandra Graß, Helmut Seidl
|
| 12:00 - 13:30 |
Lunch
|
Session 3: Keynote Session (Chair: Alessandro Pinto)
| 13:30 - 14:30 |
Hadas Kress-Gazit
Formal methods for robotics in the age of big data
|
| 14:30 - 14:45 |
Coffee Break
|
Session 4: Runtime Monitoring for Autonomous Systems (Chair: Sean Kauffman)
| 14:45 - 15:15 |
From Natural Language Requirements to Runtime Monitors for Resource-Constrained Systems: Integrating FRET and R2U2
Alexis Aurandt, Christopher Johannsen, Andreas Katis, Anastasia Mavridou, Kristin Yvonne Rozier, Phillip H. Jones
|
| 15:15 - 15:45 |
From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink
Arthur Amorim, Paul Gazzillo, Max Taylor, Lance Joneckis
|
| 15:45 - 16:15 |
Hardware-In-The-Loop Validation of Formal Models: An Application to AI-Controlled Drones
Fabian Vu, Jan Gruteser, Philipp Körner, Michael Leuschel, David Geleßus, Miles Vella
|
| 16:15 - 16:30 |
Coffee Break
|
Session 5: Stochastic & Probabilistic Formal Methods (Chair: Cesar Munoz)
| 16:30 - 17:00 |
Sensor Tolerance Contracts for Safety Assurance in Cyber-Physical Systems
Jian Xiang
|
| 17:00 - 17:30 |
Learning Probabilistic Automata from Single Continuous-Valued System Logs
Simon Dierl, Nastaran Kianersi, Falk Howar, Sean Kauffman
|
| 17:30 - 18:00 |
Formal Analysis of Stochastic Cognitive Models: A Translation Framework from Soar to PRISM
Parth Ganeriwala, Candice Chambers, James I. Lathrop, Siddhartha Bhattacharyya, Junaid Babar, Stephen Gilbert, Isaac Amundson, Michael C. Dorneich, Mohammed Abdul Hafeez Khan
|
Day 2 - May 06, 2026
Session 6: Keynote Session (Chair: Jyo Deshmukh)
| 09:00 - 10:00 |
Leonardo de Moura
Lean 4: A Unified Platform for Programming and Verification
|
| 10:00 - 10:30 |
Coffee Break
|
Session 7: Low-Level Systems & Hardware Verification (Chair: Kristin Yvonne Rozier)
| 10:30 - 11:00 |
Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving
Aaron Bembenek, Toby Murray
|
| 11:00 - 11:30 |
Multicore Scheduling for Large Safety-Critical Applications: Beyond Single-Core Equivalence
Peter Csaba Ölveczky, José Meseguer
|
| 11:30 - 12:00 |
Artificial Incorrectness: SMT and LLMs in Hardware Synthesis
Edward Wang, Joe Walston, Luca Daniel, Tony Tan, Yoni Zohar, Clark Barrett
|
| 12:00 - 13:30 |
Lunch / steering committee meeting
|
Session 8: Keynote Session (Chair: Klaus Havelund)
| 13:30 - 14:30 |
Clark Barrett
CSLib: Building a Platform for AI-assisted Formal Verification in Lean
|
| 14:30 - 14:45 |
Coffee Break
|
Session 9: Neural Network Verification & Adversarial Robustness (Chair: Jean-Baptiste Jeannin)
| 14:45 - 15:15 |
Towards Formal Verification of Deep Neural Networks for Object Detection
Avraham Raviv, Yizhak Yisrael Elboher, Omri Isac, Michelle Aluf-Medina, Ben Hagag, Golan Shmueli, Guy Katz, Hillel Kugler
|
| 15:15 - 15:45 |
Adversarial Robustness of Time-Series Classification for Crystal Collimator Alignment
Xaver Fink, Borja Fernandez Adiego, Daniele Mirarchi, Eloise Matheson, Álvaro García González, Gianmarco Ricci, Joost-Pieter Katoen
|
| 15:45 - 16:15 |
Safer Policies via Affine Representations using Koopman Dynamics
Tanmay Ambadkar, Darshan Chudiwal, Greg Anderson, Abhinav Verma
|
| 16:15 - 16:30 |
Coffee Break
|
Session 10: Program Analysis & Defect Detection (Chair: Abinav Verma)
| 16:30 - 17:00 |
Misguarded Computations: A Pattern of Ineffective Conditional Protection
Oleksandr Kolchyn, Dariia Rudenko
|
| 17:00 - 17:30 |
Quantitative Symbolic Patch Impact Analysis
Laboni Sarker, Abdus Satter, Tevfik Bultan
|
| 17:30 - 18:00 |
Evaluating Coverage and Fault Detection Capability of Scenarios for the Validation of Asmeta Specifications
Andrea Bombarda, Silvia Bonfanti, Cesar Cornejo, Angelo Gargantini, Nico Pellegrinelli
|
Day 3 - May 07, 2026
Session 11: Keynote Session (Chair: Alessandro Pinto)
| 09:00 - 10:00 |
Rahul Kumar
Verifying the Safety of the Rust Standard Library
|
| 10:00 - 10:30 |
Coffee Break
|
Session 12: Formal Semantics & Verified Tools (Chair: Laura Humphrey)
| 10:30 - 11:00 |
A Formal Semantics of C with OpenMP Parallelism
Ke Du, Anshu Sharma, Liyi Li, William Mansky
|
| 11:00 - 11:30 |
Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
Serra Zehra Dane, Jiawei Chen, Marc Pouzet, Jean-Baptiste Jeannin
|
| 11:30 - 12:00 |
Foundational VeriFast: Pragmatic Certification of Verification Tool Results through Hinted Mirroring
Bart Jacobs
|
| 12:00 - 13:30 |
Lunch
|
Session 13: Keynote Session (Chair: Jyo Deshmukh)
| 13:30 - 14:30 |
Cesar Munoz
Formal Verification in Practice: Interactive Theorem Proving for NASA Safety-Critical Systems
|
| 14:30 - 14:45 |
Coffee Break
|
Session 14: Aviation Safety & Collision Avoidance (Chair: Hadas Kress-Gazit)
| 14:45 - 15:15 |
World2Rules: A Neuro-Symbolic Framework for Learning World-Governing Safety Rules for Aviation
Haichuan Wang, Jay Patrikar, Sebastian Scherer
|
| 15:15 - 15:45 |
Compressing ACAS-Xu Lookup Tables with Binary Decision Diagrams
Martin Boniol, Julien Brunel, Jean-Baptiste Chaudron, Christophe Garion, Xavier Thirioux
|
| 15:45 - 16:15 |
Automatic Certification of the Active Corner Method for Collision Avoidance
Nishant Kheterpal, J. Tanner Slagel, Elanor Tang, Serra Zehra Dane, Jean-Baptiste Jeannin
|
| 16:15 - 16:30 |
Coffee Break
|
Session 15: Case Study and NASA Panel (Chair: Serra Dane)
| 16:30 - 17:00 |
Formal Runtime Verification of Avionics Systems Using Level-D Flight Simulator Data and NASA F Prime
Maria C. Moreno
|
| 17:00 - 17:30 |
NASA Panel: Will AI make formal methods relevant or irrelevant?
|