Complexity and Termination
Learning Probabilistic Termination Proofs
Ghost Signals: Verifying Termination of Busy Waiting
Reflections on Termination of Linear Loops
Decision Tree Learning in CEGIS-Based Termination Analysis
ATLAS: Automated Amortised Complexity Analysis of Self-Adjusting Data Structures
Decision Procedures and Solvers
Theory Exploration Powered by Deductive Synthesis
CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver
Porous Invariants
JavaSMT 3: Interacting with SMT Solvers in Java
Efficient SMT-based Analysis of Failure Propagation
ToolX : Better Delta Debugging for the SMT-LIBv2 Language and Friends
Learning Union of Integer Hypercubes with Queries (with applications to monadic decomposition)
Interpolation and Model Checking for Nonlinear Arithmetic
An SMT Solver for Regular Expressions and Linear Arithmetic over String Length
Counting Minimal Unsatisfiable Subsets
Sound Verification Procedures for Temporal Properties of Infinite-State Systems
Hardware and Model Checking
Progress in Certifying Hardware Model Checking Results
Model-Checking Structured Context-Free Languages
Model Checking! -Regular Properties with Decoupled Search
AIGEN: Random Generation of Symbolic Transition Systems
GPU Acceleration of Bounded Model Checking with ParaFROST
Pono: A Flexible and Extensible SMT-based Model Checker
Logical Foundations
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation
Formal Foundations of Fine-Grained Explainability
Latticed k-Induction with an Application to Probabilistic Programs
Stochastic Systems
Runtime Monitors for Markov Decision Processes
Model Checking Finite-Horizon Markov Chains with Probabilistic Inference
Enforcing Almost-Sure Reachability in POMDPs
Rigorous Floating-Point Roundo Error Analysis of Probabilistic Computations
Model-free Reinforcement Learning for Branching Markov Decision Processes
Software Verification
Cameleer: a Deductive Verification Tool for OCaml
LLMC: Verifying High-Performance Software
Formally Validating a Practical Verification Condition Generator
Automatic Generation and Validation of Instruction Encoders and Decoders
An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation
Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios
Functional Correctness of C implementations of Dijkstra's, Kruskal's, and Prim's Algorithms
Gillian, Part II: Real-World Verification for JavaScript and C
Debugging Network Reachability with Blocked Paths
Lower-Bound Synthesis using Loop Specialization and Max-SMT
Fast Computation of Strong Control Dependencies
Di y: Inductive Reasoning of Array Programs using Difference Invariants.