Accepted Papers

1. 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

2. Misguarded Computations: A Pattern of Ineffective Conditional Protection
   Oleksandr Kolchyn, Dariia Rudenko

3. Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving
   Aaron Bembenek, Toby Murray

4. Sensor Tolerance Contracts for Safety Assurance in Cyber-Physical Systems
   Jian Xiang

5. 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

6. World2Rules: A Neuro-Symbolic Framework for Learning World-Governing Safety Rules for Aviation
   Haichuan Wang, Jay Patrikar, Sebastian Scherer

7. Compressing ACAS-Xu Lookup Tables with Binary Decision Diagrams
   Martin Boniol, Julien Brunel, Jean-Baptiste Chaudron, Christophe Garion, Xavier Thirioux

8. 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

9. DisQ: A Model of Distributed Quantum Processors
   Le Chang, Saitej Yavvari, W. Rance Cleaveland, Samik Basu, Runzhou Tao, Liyi Li

10. 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

11. A Formal Semantics of C with OpenMP Parallelism
    Ke Du, Anshu Sharma, Liyi Li, William Mansky

12. Quantitative Symbolic Patch Impact Analysis
    Laboni Sarker, Abdus Satter, Tevfik Bultan

13. Multicore Scheduling for Large Safety-Critical Applications: Beyond Single-Core Equivalence
    Peter Csaba Ölveczky, José Meseguer

14. Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
    Serra Zehra Dane, Jiawei Chen, Marc Pouzet, Jean-Baptiste Jeannin

15. From High-Level Types to Low-Level Monitors: Synthesizing Verified Runtime Checkers for MAVLink
    Arthur Amorim, Paul Gazzillo, Max Taylor, Lance Joneckis

16. Safer Policies via Affine Representations using Koopman Dynamics
    Tanmay Ambadkar, Darshan Chudiwal, Greg Anderson, Abhinav Verma

17. 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

18. Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition
    William Schultz, Edward Ashton, Heidi Howard, Stavros Tripakis

19. Learning Probabilistic Automata from Single Continuous-Valued System Logs
    Simon Dierl, Nastaran Kianersi, Falk Howar, Sean Kauffman

20. Automatic Certification of the Active Corner Method for Collision Avoidance
    Nishant Kheterpal, J. Tanner Slagel, Elanor Tang, Serra Zehra Dane, Jean-Baptiste Jeannin

21. Formal Runtime Verification of Avionics Systems Using Level-D Flight Simulator Data and NASA F Prime
    Maria C. Moreno

22. Evaluating coverage and fault detection capability of scenarios for the validation of Asmeta specifications
    Andrea Bombarda, Silvia Bonfanti, Cesar Cornejo, Angelo Gargantini, Nico Pellegrinelli

23. Foundational VeriFast: Pragmatic Certification of Verification Tool Results through Hinted Mirroring
    Bart Jacobs

24. Verifying a Solver for Mixed Flow-Sensitive Analyses
    Sarah Tilscher, Alexandra Graß, Helmut Seidl

25. Artificial Incorrectness: SMT and LLMs in Hardware Synthesis
    Edward Wang, Joe Walston, Luca Daniel, Tony Tan, Yoni Zohar, Clark Barrett