| Keynote |
| 8:50 – 9:00 | Opening Remarks |
| 9:00 – 10:00 | Keynote – Darren Cofer |
| 10:00 – 10:30 | Break |
| Theorem Proving |
| 10:30 – 11:00 |
Ziggy Attala, Fang Yan, Simon Foster, Ana Cavalcanti and Jim Woodcock.
Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software. |
| 11:00 – 11:30 |
Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin, Bernhard Scholz and Pavle Subotic.
Reusable Formal Verification of DAG-based Consensus Protocols. |
| 11:30 – 12:00 |
Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Maria Júlia Dias Lima, Mariano Moscato and Temur Kutsia.
Verification of an Anti-Unification Algorithm in PVS. |
| 12:00 – 1:30 |
Lunch |
| Verification |
| 1:30 – 2:00 |
Elias Khalife, Pierre-Loic Garoche and Mazen Farhood.
Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints. |
| 2:00 – 2:30 |
Sumio Morioka, Satoshi Obana and Maki Yoshida.
Formal Verification of Composite Field Multipliers for Information-Theoretically Secure Radio Communication in Spacecraft Control. |
| 2:30 – 2:45 |
Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Matias Salinas and Christine Betz.
Formal Verification as a Service: A CERN-GSI Case Study. |
| 2:45 – 3:00 |
Calvin Beck, Hanxi Chen and Steve Zdancewic.
Vellvm: Formalizing the Informal LLVM (Experience Report). |
| 3:00 – 3:30 | Break |
| SAT/SMT |
| 3:30 – 4:00 |
Max Bannach, Jai Grover and Markus Hecher.
Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators. |
| 4:00 – 4:30 |
Benjamin Valpey, Xinyi Li, Sreepathi Pai and Ganesh Gopalakrishnan.
An SMT Formalization of Mixed-Precision Matrix Multiplication (Modeling Three Generations of Tensor Cores). |
| 4:30 – 5:00 |
Sarat Chandra Varanasi, Baoluo Meng, Robert Lorch, Abha Moitra, Kit Siu, Saswata Paul, Michael Durling, Neha Beniwal and Nikita Visnevski.
TRACE: Toolkit for Requirements Analysis, Capture, and Elicitation. |
| Keynote |
| 8:50 – 9:00 | Opening Remarks |
| 9:00 – 10:00 | Keynote – Emina Torlak. Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. |
| 10:00 – 10:30 | Break |
| State Machines and Automata |
| 10:30 – 11:00 |
Michal Šedý and Lukáš Holík.
Automata Size Reduction by Procedure Finding. |
| 11:00 – 11:30 |
Matías Brizzio, Felipe Gorostiaga, Cesar Sanchez and Renzo Degiovanni.
Mode-based Reactive Synthesis. |
| 11:30 – 12:00 |
Mohit Tekriwal and Matthew Sottile.
Mechanized RS274 semantics for additive manufacturing. |
| 12:00 – 1:30 |
Lunch |
| Hybrid Systems |
| 1:30 – 2:00 |
Jainta Paul, Stefan Mitsch and Luis Garcia.
HyTwin: A Formal Semantics for Digital Twin Interventions in ICS Based on Time-to-Violation. |
| 2:00 – 2:30 |
Jian Xiang and Stephen Chong.
Extending Dynamic Logics with First-Class Relational Reasoning. |
| 2:30 – 3:00 |
Mathis Niehage, Carina da Silva, Anne Remke and Arnd Hartmanns.
Rare Event Simulation for Stochastic Hybrid Systems using Symbolic Importance Functions. |
| 3:00 – 3:30 | Break |
| Discrete Systems |
| 3:30 – 4:00 |
Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini and Nico Pellegrinelli.
Eliminating flakiness: deterministic control for validating nondeterministic Asmeta specifications. |
| 4:00 – 4:30 |
Edward Kim, Devan Shanker, Varun Bharadwaj, Hongbeen Park, Jinkyu Kim, Hazem Torfah, Daniel Fremont and Sanjit Seshia.
Querying Labeled Time Series Data with Scenario Programs. |
| 4:30 – 5:00 |
Carlos Olarte, Daniel Osorio, Carlos Ramirez and Camilo Rocha.
Algorithmic Analysis of Event-B in Rewriting Logic. |
| Keynote |
| 8:50 – 9:00 | Opening Remarks |
| 9:00 – 10:00 | Keynote – Natasha Neogi and Paul Miner |
| 10:00 – 10:30 | Break |
| Runtime Verification |
| 10:30 – 11:00 |
Alexis Aurandt, Phillip Jones and Kristin Yvonne Rozier.
Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust. |
| 11:00 – 11:15 |
Arthur Amorim, Max Taylor, Trevor Kann, William Harrison, Gary Leavens and Lance Joneckis.
Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types. |
| 11:15 – 11:30 |
Nafiz Sadman, Nastaran Kianersi and Sean Kauffman.
Visualizing Temporal Interval Hierarchies. |
| 11:30 – 12:00 | Break |
| Temporal Logics |
| 12:00 – 12:30 |
Andreas Katis, Anastasia Mavridou and Thomas Pressburger.
A Streamlined, Formal Approach to Requirements-based Testing. |
| 12:30 – 1:00 |
Alec Rosentrater, Zili Wang, Katherine Kosaian and Kristin Yvonne Rozier.
Language Partitioning for Mission-time Linear Temporal Logic. |
| 1:00 – 1:10 | Closing Remarks |