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 Büchi Automata based on SCC Decomposition.- Complementing Büchi 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