Computer Aided Verification

A Billion SMT Queries a Day.- Program Verification with Constrained Horn Clauses.- Formal Methods for Probabilistic Programs Data-Driven Invariant Learning for Probabilistic Programs.- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs.- Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions.- Abstraction-Renement for Hierarchical Probabilistic Models.- Formal Methods for Neural Networks Shared Certificates for Neural Network Verification.- Example Guided Synthesis of Linear Approximations for Neural Network Verification.- Verifying Neural Networks Against Backdoor Attacks.- Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning.- Neural Network Robustness as a Verication Property: A Principled Case Study.- Software Verication and Model Checking The Lattice-Theoretic Essence of Property Directed Reachability Analysis.- A-ne Loop Invariant Generation via Matrix Algebra.- Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes.- Proof-guided Underapproximation Widening for Bounded Model Checking.- SolCMC: Solidity Compiler''s Model Checker.- Sharygina Hyperproperties and Security Software Verication of Hyperproperties Beyond k-Safety.- Abstraction Modulo Stability for Reverse Engineering.- A Modular and Highly Extensible API Fuzzer for SMT Solvers.- Automata and Logic FORQ-based Language Inclusion Formal Testing.- Sound Automation of Magic Wands.- Divide-and-Conquer Determinization of Buchi Automata based on SCC Decomposition.- Complementing Buchi Automata with Ranker.- Deductive Verication and Decision Procedures Even Faster Conicts and Lazier Reductions for String Solvers.- Local Search For SMT on Linear Integer Arithmetic.- Reasoning about Data Trees using CHCs.- Veried Erasure Correction in Coq with MathComp and VST.- Appel End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers.- A DSL and Verication Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols.- Machine Learning Specication-Guided Learning of Nash Equilibria with High Social Welfare.- Synthesizing Fair Decision Trees via Iterative Constraint Solving.- SMT-based Translation Validation for Machine Learning Compiler.- Lee Verifying Fairness in Quantum Machine Learning.- MoGym: Using Formal Models for Training and Verifying Decision-making Agents.- Synthesis and Concurrency Synthesis and Analysis of Petri Nets from Causal Specications.- Verifying generalised and structural soundness of workow nets via relaxations.- Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET.- Information Flow Guided Synthesis.- Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation.