Program

10:30-10:45 On the Complexity of Checking Soundness of Natural Reductions
10:45-11:00 Deadlock Verification via Ordering-Constrained Mutex Modeling
11:00-11:15 Complete Local Reasoning About Parameterized Programs Over Topologies
11:15-11:30 Scalable Deductive Verification of Data-Level Parallel Programs
11:30-11:45 On the Verification Problem of Remote Direct Memory Access programs
11:45-11:55 Model Checking for Flexible Network Protocols
11:55-12:05 The TLA+ Model Checker Apalache
12:05-12:15 PSF: A Generic and Extensible Framework for Protocol State Fuzzing
12:15-12:25 Kofola 1.0: A Modular Approach to 𝝎-Regular Complementation and Inclusion Checking
12:25-12:35 Octopus: Practical Equivalence Checking of P4 Packet Parsers

14:00-14:15 Randomise Alone, Reach Together
14:15-14:30 Decoupled Planning for Multiple Omega-Regular Objectives
14:30-14:45 Repairing Regex-Dependent String-Manipulation Programs
14:45-15:00 Liquid Tree Automata
15:00-15:10 SemML 2.0: Synthesizing Controllers from LTL
15:10-15:20 Fast Obligation Translation and Synthesis
15:20-15:30 sweap: Reactive Synthesis for Infinite-State Integer Problems

16:00-16:15 A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking
16:15-16:30 A Multi-Width Parametric Equivalence Solver
16:30-16:45 Massively Parallel Mining of Specifications for Hardware Designs
16:45-17:00 A mechanised, bidirectional type system for bit-width determination in SystemVerilog

10:30-10:45 Differentially Private Runtime Monitoring
10:45-11:00 HyperLasso: Bounded Model Checking of ∀+∃+-Liveness Hyperproperties
11:00-11:10 The Simulator’s Blueprint: Automata Learning from Cybersecurity Logs
11:10-11:20 HyperQB 2.0: A Bounded Model Checker for Hyperproperties

11:20-11:35 Improving Stability of SMT Solvers via Context-Driven Normalization
11:35-11:50 Satisfiability Modulo Extensional Constant Arrays
11:50-12:05 String Solving with Stabilization and Transducers
12:05-12:20 Lagrangian-Based Duality for Quantified SMT Algorithms
12:20-12:30 Mallob: Scalable Automated Reasoning On Demand

14:00-14:15 Modular Reasoning about Object Relations
14:15-14:30 Formally Verified Linear-Time Invertible Lexing
14:30-14:45 Automating Bitvector and Finite Field Equivalence Proofs in Lean
14:45-15:00 The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver
15:00-15:10 Burrow: A Proof Framework for Weak Memory
15:10-15:20 Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean
15:20-15:30 Automatic Heap-Memory Diagrams for Separation-Logic Proofs

16:00-16:15 An L# Based Algorithm for Active Learning of Minimal Separating Automata
16:15-16:30 Upper Bound for the Determinization of Emerson-Lei Automata: A One-Fin Approach
16:30-16:45 SMT-Based Active Learning of Weighted Automata
16:45-17:00 Compositional Verification of Timed Automata via Violation Assumptions
17:00-17:15 Weighted soundness for Workflow Nets
17:15-17:30 Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning
17:30-17:40 TACO: A Toolsuite for the Verification of Threshold Automata
17:40-17:50 Extending QuAK with Nested Quantitative Automata

10:30-10:45 VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification
10:45-11:00 QAV-FT: Quadratic Approximation-based Neural Network Verification via Fourier Series and Taylor Truncation
11:00-11:15 The Rocq-NN-Roll Prover: Soundly Verifying Hyperproperties of Neural Networks in Rocq
11:15-11:30 ATKVerifier: Adaptive Top-K Constraints for Tighter Verification of Semantic Segmentation Networks
11:30-11:45 Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement
11:45-12:00 Quantifying Sensitivity for Tree Ensembles : A symbolic and compositional approach
12:00-12:15 Shields to Guarantee Probabilistic Safety in MDPs
12:15-12:25 A Neurosymbolic Approach to Natural Language Formalization and Verification

14:50-15:05 Liveness Proofs for Hardware Model Checking
15:05-15:20 Transition Invariants Revisited: Termination Witnesses and Their Validation
15:20-15:30 KoAT: Automatic Complexity and Termination Analysis of Integer Programs

16:00-16:15 Sound and Precise Symbolic Automata Model for Stateful Software Systems
16:15-16:30 Automated Amortised Analysis of Skew Heaps and Leftist Heaps
16:30-16:45 Polynomial Invariant Generation for Floating-Point Programs
16:45-17:00 Parallel Abstract Interpretation for Polynomial Programs with Range Bound Assertions
17:00-17:15 Incremental Inference for Probabilistic Datalog
17:15-17:25 Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers

10:30-10:45 Consistency-Based Software Diagnosis: Accuracy, Scalability, and Limitations
10:45-10:55 Show Me The Money: An Exercise in Proof-Driven Software Understanding
10:55-11:05 SvLibChecker: A Light-Weight Tool for Software Model Checking
11:05-11:15 PyCHC: a Framework for Certified Horn Solving and CHC-based Design

11:15-11:30 How Many Circuit Identities Are Needed to Generate All Others?
11:30-11:45 A Practical Specification Language for Automatic Quantum Program Verification
11:45-12:00 Formal Verification of Quantum Ancilla Safety
12:00-12:15 Model Checking Matrix Product States Against Linear Chain Logic
12:15-12:25 Analysis and Verification of Quantum Communication Protocols in UPPAAL
12:25-12:35 Quokka#: Quantum Computing with #SAT

14:00-14:15 Over-approximation of weakly-hard constraints for control systems verification
14:15-14:30 Spatiotemporal Robustness of Temporal Logic Tasks using Multi-Objective Reasoning
14:30-14:45 Best-Effort Safety Control of Multi-Mode Systems
14:45-15:00 Perception with Guarantees: Certified Pose Estimation via Reachability Analysis
15:00-15:15 Tensor Probabilistic Model Checking of Finite-Horizon Markov Chains
15:15-15:30 Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families
15:30-15:40 Ensuring Safety in Automotive Machine Learning Inference: From Pre-validated Static Kernels to Machine Learning Graph Compilation
15:40-15:50 Caesar: A Deductive Verifier for Probabilistic Programs
15:50-16:00 ULTIMATE: A Tool for the Verification and Synthesis of Stochastic World Models