Computer Aided Verification

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.