Keynotes
Symbolic Computation in Automated Program Reasoning
The next big thing: from embedded systems to embodied actors
Intelligent and Dependable Decision-Making Under Uncertainty
A Coq formalization of Lebesgue Induction Principle and Tonellis Theorem
SAT/SMT
Railway Scheduling Using Boolean Satisfiability Modulo Simulations
SMT Sampling via Model-Guided Approximation
Efficient SMT-based Network Fault Tolerance Verification
Verification I
Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems
Can we Communicate? Using Dynamic Logic to Verify Team Automata
The ScalaFix equation solver
HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
Quantitative Verification
symQV: Automated Symbolic Verification of Quantum Programs
PFL: a Probabilistic Logic for Fault Trees
Energy Buechi Problems
QMaude: quantitative specification and verification in rewriting logic
Concurrency and Memory Models
Minimisation of Spatial Models using Branching Bisimilarity
Reasoning about Promises in Weak Memory Models with Event Structures
A fine-grained semantics for arrays and pointers under weak memory models
VeyMont: Parallelising Verified Programs instead of Verifying Parallel Programs
Verification 2
Verifying At the Level of Java Bytecode
Abstract Alloy Instances
Monitoring the Internet Computer
Word Equations in Synergy with Regular Constraints
Formal Methods in AI
Verifying Feedforward Neural Networks for Classification in Isabelle/HOL
SMPT: A Testbed for Reachabilty Methods in Generalized Petri Nets
The Octatope Abstract Domain for Verification of Neural Networks
Program Semantics and Verification Technique for AI-centred Programs
Safety and Reliability
Tableaux for Realizability of Safety Specifications
A Decision Diagram Operation for Reachability
Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B Refinement
A Runtime Environment for Contract Automata
Industry Day
Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny
Shifting Left for Early Detection of Machine-Learning Bugs
A Systematic Approach to Automotive Security
Specification-Guided Critical Scenario Identification for Automated Driving
Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks
Backdoor Mitigation in Deep Neural Networks via Strategic Retraining
veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System.