- Monitoring Extended Hypernode Logic, Marek Chalupa, Thomas Henzinger and Ana Oliveira da Costa
- A Formal Tainting-Based Framework for Malware Analysis, Andrei-Catalin Mogage and Dorel Lucanu
- Implementing, Specifying, and Verifying the QOI Format in Dafny: A Case Study, Stefan Ciobaca and Diana-Elena Gratie
- VeriCode: Correct Translation of Abstract Specifications to C Code, Gerhard Schellhorn, Stefan Bodenmüller and Wolfgang Reif
- Stateful Functional Modeling with Refinement (a Lean4 framework), Frederic Peschanski
- Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods, George Granberry, Wolfgang Ahrendt and Moa Johansson
- Towards Quantitative Analysis of Simulink Models using Stochastic Hybrid Automata, Pauline Blohm, Paula Herber and Anne Remke
- Modeling Register Pairs in CompCert, Alexander Loitzl and Florian Zuleger
- VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory, Robert Rubbens, Petra van den Bos and Marieke Huisman
- Correct and Complete Symbolic Execution for Free, Erik Voogd, Einar Broch Johnsen, Åsmund Aqissiaq Arild Kløvstad, Jurriaan Rot and Alexandra Silva
- Monitoring Real-Time Systems under Parametric Delay, Martin Fränzle, Thomas Møller Grosen, Kim Guldstrand Larsen and Martin Zimmermann
- PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases, Logan Murphy, Torin Viger, Alessio Di Sandro and Marsha Chechik
- Solvent: liquidity verification of smart contracts, Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini and Vadim Malvone
- Proving Termination via Measure Transfer in Equivalence Checking, Dragana Milovančević, Carsten Fuhs, Mario Bucev and Viktor Kunčak
- PyQBF: A Python Framework for Solving Quantified Boolean Formulas, Mark Peyrer, Maximilian Heisinger and Martina Seidl
- Improving SAT Solver Performance through MLP-Predicted Genetic Algorithm Parameters, Sabrine Saouli, Souheib Baarir and Claude Dutheillet
- A Systematic Literature Review on a Decade of Industrial TLA+ Practice, Roman Bögli, Leandro Lerena, Christos Tsigkanos and Timo Kehrer
- Active Learning of Runtime Monitors Under Uncertainty, Sebastian Junges, Sanjit A. Seshia and Hazem Torfah
- STEVE: A Rational Verification Tool for Stackelberg Security Games, Surasak Phetmanee, Michele Sevegnani and Oana Andrei
