- Lidia Losavio, Marco Paganoni and Carlo A. Furia
Model-Based Testing of an Intermediate Verifier Using Executable Operational Semantics
- Jorge Blázquez Saborido, Manuel Montenegro and Clara Segura
Verified Implementation of Associative Containers with Iterators Using Threaded Red-Black Trees
- Reiner Hähnle, Cosimo Laneve and Adele Veschetti
Formal Verification of Legal Contracts: A Translation-based Approach
- Matthias Grundmann and Hannes Hartenstein
Security of the Lightning Network: Model Checking a Stepwise Refinement with TLA+
- Martin Hána, Nikolai Kosmatov, Julien Signoles and Virgile Prevosto
Formal Verification of PKCS#1 Signature Parser using Frama-C
- Jean-Christophe Filliatre, Andrei Paskevich and Olivier Danvy
When Separation Arithmetic is Enough
- Manar Altamimi, Asieh Salehi Fathabadi and Vahid Yazdanpanah
Formal Modeling of Trust in AI-Driven Autonomous Delivery Vehicles
- Chelsea Edmonds, John Derrick, Brijesh Dongol, Gerhard Schellhorn and Heike Wehrheim
Model Checking Buffered Durable Linearizability in CSP
- Georgiana Caltais, Andrei Covaci and Hossein Hojjat
Concurrency Under Control: Systematic Analysis of SDN Race Hazards
- Gabriel Dengler, Sven Apel and Holger Hermanns
Automata Learning – Expect Delays!
- Konstantin Britikov, Grigory Fedyukovich and Natasha Sharygina
CHC-Based Reachability Analysis via Cycle Summarization
- David Cortés, Jean Leneutre, Vadim Malvone, James Ortiz and Pierre-Yves Schobbens
Extending Timed Automata with Clock Derivatives
- Michele Alberti, François Bobot, Julien Girard-Satabin, Alban Grastien, Aymeric Varasse and Zakaria Chihani
The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification
- Giuseppe De Palma, Saverio Giallorenzo, Jacopo Mauro, Matteo Trentin and Gianluigi Zavattaro
Reachability Analysis of Function-as-a-Service Scheduling Policies
- Ion Chirica and Mário Pereira
Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
- Sophie Rain, Anja Petković Komel, Michael Rawson and Laura Kovács
Game Modeling of Blockchain Protocols
- Carlos Isasa, Noah Abou El Wafa, Cláudio Gomes, Peter Gorm Larsen and André Platzer
Safe Temperature Regulation: Formally Verified and Real-World Validated
- Angelo Ferrando, Peng Lu and Vadim Malvone
Auto-Generating Visual Editors for Formal Logics with Blockly
- Neda Saeedloei and Feliks Kluzniak
Distributed Timed Scenarios
- Eshita Zaman, Christopher Johannsen, Andrew S Miner, Gianfranco Ciardo and Samik Basu
CTL Model Checking Partially Specified Systems
- Jonathan Hellwig, Lukas Schäfer, Long Qian, Matthias Althoff and André Platzer
From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes
- Douglas Fraser, Alice Miller, Marco Cook and Dimitrios Pezaros
Online Model Checking for Anomaly Detection in Industrial Control Systems
- Fletcher Chapin, Ankur Varma, Samuel Akinwande, Meagan Mauter and Sriram Sankaranarayanan
Using Bayesian Inference and Flowpipe Construction to Bound Predictions of Biogas Production at Wastewater Treatment Plants
- Gidon Ernst and Grigory Fedyukovich
Quick Theory Exploration for Algebraic Data Types via Program Transformations