Linked e-resources
Details
Table of Contents
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
Ane 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.
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
Ane 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.