| Density of Reachable States and How to Use it for Safe Autonomous Motion Planning | Yue Meng, Zeng Qiu, Md Tawhid Bin Waez and Chuchu Fan. |
| From Verified Scala to STIX File System Embedded Code using Stainless | Jad Hamza, Simon Felix, Viktor Kuncak, Ivo Nussbaumer and Filip Schramka. |
| Operational annotations: a new method for sequential program verification | Paul Attie. |
| Robust Computation Tree Logic | Satya Prakash Nayak, Daniel Neider, Rajarshi Roy and Martin Zimmermann. |
| Zone extrapolations in parametric timed automata | Johan Arcile and Étienne André. |
| More Programming Than Programming: Teaching Formal Methods in a Software Engineering Programme | James Noble, David Streader, Isaac Oscar Gariano and Miniruwani Samarakoon. |
| Towards Refactoring FRETish Requirements | Marie Farrell, Matt Luckcuck, Oisin Sheridan and Rosemary Monahan. |
| Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda | Harold Carr, Christopher Jenkins, Mark Moir, Victor Cacciari Miraldo and Lisandra Silva. |
| Assume-Guarantee Reasoning with Scheduled Components | Cong Liu, Junaid Babar, Isaac Amundson, Karl Hoech, Darren Cofer and Eric Mercer. |
| On-the-Fly Model Checking with Neural MCTS | Ruiyang Xu and Karl Lieberherr. |
| Permutation Invariance of Deep Neural Networks with ReLUs | Diganta Mukhopadhyay, Kumar Madhukar and Mandayam Srivas. |
| On the Termination of Borrow Checking in Featherweight Rust | Etienne Payet, David J. Pearce and Fausto Spoto. |
| The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS | Usama Mehmood, Sanaz Sheikhi, Stanley Bak, Scott Smolka and Scott Stoller. |
| Towards Better Test Coverage: Merging Unit Tests for Autonomous Systems | Josefine Graebener, Apurva Badithela and Richard Murray. |
| DSV: Disassembly Soundness Validation without Assuming a Ground Truth | Xiaoxin An, Freek Verbeek and Binoy Ravindran. |
| Closed-Loop ACAS Xu NNCS is Unsafe: Quantized State Backreachability for Verification | Stanley Bak and Hoang Dung Tran. |
| Approximate Translation from Floating-Point to Real-Interval Arithmetic | Daisuke Ishii, Takashi Tomita and Toshiaki Aoki. |
| Hierarchical Contract-based Synthesis for Assurance Cases | Timothy Wang, Zamira Daw, Pierluigi Nuzzo and Alessandro Pinto. |
| Stateful Black-Box Fuzzing of Bluetooth Devices Using Automata Learning | Andrea Pferscher and Bernhard K. Aichernig. |
| Quantification of Battery Depletion Risk Made Efficient | Gilles Nies and Holger Hermanns. |
| Configurable Benchmarks for C Model Checkers | Xaver Fink, Philipp Berger and Joost-Pieter Katoen. |
| Timed Automata Learning via SMT Solving | Martin Tappler, Bernhard K. Aichernig and Florian Lorber. |
| Verified Probabilistic Policies for Deep Reinforcement Learning | Edoardo Bacci and David Parker. |
| Asynchronous Composition of Local Interface LTL Properties | Alberto Bombardelli and Stefano Tonetta. |
| Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan and Marielle Stoelinga. | BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees |
| Exemplifying parametric timed specifications over signals with bounded behavior | Étienne André, Masaki Waga, Natsuki Urabe and Ichiro Hasuo. |
| Monitorability of Expressive Verdicts | Felipe Gorostiaga and Cesar Sanchez. |
| Requirements-Driven Model Checking and Test Generation for Comprehensive Verification | Devesh Bhatt, Hao Ren, Anitha Murugesan, Jason Biatek, Srivatsan Varadarajan and Natrajan Shankar. |
| Probabilistic Hyperproperties with Rewards | Lukas Wilke, Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci and Borzoo Bonakdarpour. |
| Hypercontracts | Inigo Incer, Albert Benveniste, Alberto Sangiovanni-Vincentelli and Sanjit Seshia. |
| Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry | Zachary Luppen, Michael Jacks, Nathan Baughman, Muhamed Stilic, Ryan Nasers, Benjamin Hertz, James Cutler, Dae Young Lee and Kristin Yvonne Rozier. |
| Runtime Verification Triggers Real-time, Autonomous Fault Recovery on the CySat-I | Alexis Aurandt, Phillip Jones and Kristin Yvonne Rozier. |
| Incremental Transitive Closure for Zonal Abstract Domain | Kenny Ballou and Elena Sherman. |
| NNLander-VeriF: A Neural Network Formal Verification Framework for Vision-Based Autonomous Aircraft Landing | Ulices Santa Cruz Leal and Yasser Shoukry. |
| The Power of Disjoint Support Decompositions in Decision Diagrams | Lieuwe Vinkhuijzen and Alfons Laarman. |
| Proof Mate: an Interactive Proof Helper for PVS | Paolo Masci and Aaron Dutle. |
| Certified Computation of Nondeterministic Limits | Michal Konecny, Sewon Park and Holger Thies. |
| ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs | Christopher Strong, Sydney Katz, Anthony Corso and Mykel Kochenderfer. |
| Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT | Baoluo Meng, Arjun Viswanathan, William Smith, Abha Moitra, Kit Siu and Michael Durling. |