CAV2024: 36TH INTERNATIONAL CONFERENCE ON COMPUTER AIDED VERIFICATION

This page contains an index consisting of author-provided keywords.

#
#SAT	Simulating Quantum Circuits by Model Counting
A
Abstract Interpretation	General Anticipatory Runtime Verification Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
Abstraction	Bisimulation Learning
access control	(Recorded) Probabilistic Access Policies with Automated Reasoning Support
access policies	(Recorded) Probabilistic Access Policies with Automated Reasoning Support
accountable software systems	soid: A Tool for Legal Accountability for Automated Decision Making
Adversarial attacks safety	Boosting Few-Pixel Robustness Verification via Covering Verification Designs
almost-sure termination	Lexicographic Ranking Supermartingales with Lazy Lower Bounds
approximate model counting	(Distinguished Paper) Formally Certified Approximate Model Counting
Approximating Reasoning	Approximate Relational Reasoning for Quantum Programs
APR	Syntax-Guided Automated Program Repair For Hyperproperties
artificial intelligence	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks How to Solve Math Problems without Talent
automata theory	Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automaton
automata-logic connection	Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
Automated Program Verification	(Distinguished Paper) A Framework for Debugging Automated Program Verification Proofs via Proof Actions
automated reasoning	(Recorded) Probabilistic Access Policies with Automated Reasoning Support Lean 4: Bridging Formal Mathematics and Software Verification Realizing Leibniz’s Dream
Automated verification	Verifying Cake Cutting, Faster
Autonomous Aircraft	Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
Award CAV	CAV Award Talk
B
Bayes error	Certified Robust Accuracy of Neural Networks Are Bounded due to Bayes Errors
Binary decision diagram	Dynamic Programming for Symbolic Boolean Realizability and Synthesis
bit-blasting	Scalable Bit-Blasting with Abstractions
bit-vectors	Scalable Bit-Blasting with Abstractions
Blockchain	(Recorded) hevm, a Fast Symbolic Execution Framework for EVM Bytecode
Boolean synthesis	Dynamic Programming for Symbolic Boolean Realizability and Synthesis
Bucket elimination	Dynamic Programming for Symbolic Boolean Realizability and Synthesis
C
Cardinality constraints	From Clauses to Klauses
Causality	Synthesis of Temporal Causality
CAV	CAV Award Talk Opening Remarks
CAV Award	CAV Award Talk
CDCL	Arithmetic Solving in Z3
certified training	Certified Robust Accuracy of Neural Networks Are Bounded due to Bayes Errors
CNF Encoding	From Clauses to Klauses
collective	Collective Contracts for Message-Passing Parallel Programs
commutativity	Predictive Monitoring with Strong Trace Prefixes
competition	The Reactive Synthesis Competition (SYNTCOMP) Report
Compiler verification	Strided Difference Bound Matrices
Compilers for ML	Strided Difference Bound Matrices
Compositional Synthesis	Information Flow guided Synthesis with Unbounded Communication
compositionality	Compositional Value Iteration with Pareto Caching
computer algebra	How to Solve Math Problems without Talent
concurrency	Predictive Monitoring with Strong Trace Prefixes The VerCors Verifier: a Progress Report
Concurrency Shared Memory	Parsimonious Optimal Dynamic Partial Order Reduction
Congruence Constraint Systems	Strided Difference Bound Matrices
Constrained Horn Clauses	SolTG: A CHC-based Solidity Test Case Generator
contract	Collective Contracts for Message-Passing Parallel Programs
Controller Synthesis	Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models
Coq	(Recorded) End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT
correctness proof	The Top-Down Solver Verified: Building Confidence in Static Analyzers
cs and law	soid: A Tool for Legal Accountability for Automated Decision Making
Cyber Physical System	(Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
cyber-physical system	Optimization-Based Model Checking for Complex STL Specifications
D
Data-driven verification	Bisimulation Learning
Decidable Logics	Toward Liveness Proofs at Scale
deductive software verification	The VerCors Verifier: a Progress Report
Deductive Verification	Toward Liveness Proofs at Scale
Deep Learning	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Difference Bound Matrices	Strided Difference Bound Matrices
Distributed Synthesis	Information Flow guided Synthesis with Unbounded Communication
DNN-controlled Systems	Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
dynamic analysis	Predictive Monitoring with Strong Trace Prefixes
Dynamic programming	Dynamic Programming for Symbolic Boolean Realizability and Synthesis
E
eBPF	(Recorded) End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT
Enumerative	The SemGuS Toolkit
EVM	(Recorded) hevm, a Fast Symbolic Execution Framework for EVM Bytecode
F
F*	(Distinguished Paper) (Recorded) Interactive Theorem Proving modulo Fuzzing
Fair division	Verifying Cake Cutting, Faster
Falsification	(Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
Finite Fields	Split Gröbner Bases for Satisfiability Modulo Finite Fields
first-order logic	Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
first-order transition system	mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
fixpoint algorithm	The Top-Down Solver Verified: Building Confidence in Static Analyzers
Formal Methods	SMLP: Symbolic Machine Learning Prover
Formal modeling	(Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
formal verification	(Distinguished Paper) Formally Certified Approximate Model Counting
Framework	The SemGuS Toolkit
Fuzzing	(Distinguished Paper) (Recorded) Interactive Theorem Proving modulo Fuzzing
G
game theory	Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement
Global robustness	(Recorded) Verifying Global Two-Safety Properties in Neural Networks with Confidence
GPU	LTL learning on GPUs
graph neural networks	(Distinguished Paper) Regular Reinforcement Learning
Groebner Bases	Split Gröbner Bases for Satisfiability Modulo Finite Fields
H
Hardware Verification	Avoiding the Shoals - A New Approach to Liveness Checking Toward Liveness Proofs at Scale
heap representation	Verification Algorithms for Automated Separation Logic Verifiers
Hybrid systems verification	Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems
HyperLTL	Syntax-Guided Automated Program Repair For Hyperproperties
Hyperparameter Tuning	Monitizer: Automating Design and Evaluation of Neural Network Monitors
Hyperproperties	(Recorded) Verifying Global Two-Safety Properties in Neural Networks with Confidence Information Flow guided Synthesis with Unbounded Communication
I
Incremental Solving	CaDiCaL 2.0
Infinite State Systems	Toward Liveness Proofs at Scale
infinite-duration games	Localized Attractor Computations for Infinite-State Games
infinite-state games	Localized Attractor Computations for Infinite-State Games
Information-flow	Information Flow guided Synthesis with Unbounded Communication
Information-flow security	Syntax-Guided Automated Program Repair For Hyperproperties
Inner-approximations	(Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
Integer polyhedra	Strided Difference Bound Matrices
Interactive Theorem Proving	(Distinguished Paper) (Recorded) Interactive Theorem Proving modulo Fuzzing
Intermediate Language	Symbolic Model-Checking Intermediate-Language Tool Suite
Interval Constraint Propagation	(Distinguished Paper) (Recorded) Distributed SMT Solving Based on Dynamic Variable-level Partitioning
invariant inference	Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
ivy	mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
J
JIT	(Recorded) End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT
L
large language models	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification Guiding Enumerative Program Synthesis with Large Language Models Realizing Leibniz’s Dream
law	Realizing Leibniz’s Dream
legacy systems	Testing the migration from analog to software-based Railway Interlocking Systems
legal reasoning	Realizing Leibniz’s Dream
lexicographic ranking functions	(Recorded) Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates
linear arithmetic	Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement
linear integer arithmetic	Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
Linear temporal logic	Stochastic Omega-Regular Verification and Control with Supermartingales LTL learning on GPUs Synthesis of Temporal Causality Symbolic Model-Checking Intermediate-Language Tool Suite
Linear-time Temporal Logic	(Recorded) Measurement-based Verification of Quantum Markov Chains
Liveness Property Verification	Avoiding the Shoals - A New Approach to Liveness Checking
Liveness Verification	Toward Liveness Proofs at Scale
Local robustness analysis	Boosting Few-Pixel Robustness Verification via Covering Verification Designs
location-based access control	(Recorded) Probabilistic Access Policies with Automated Reasoning Support
Logic	Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement
LTL	LTL learning on GPUs
M
Machine Learning	LTL learning on GPUs
machine learning based access control	(Recorded) Probabilistic Access Policies with Automated Reasoning Support
Machine Learning Models	SMLP: Symbolic Machine Learning Prover
Many-valued temporal logic	Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems
Martingale theory	Stochastic Omega-Regular Verification and Control with Supermartingales
mathematical problems	How to Solve Math Problems without Talent
Mazurkiewicz traces	Predictive Monitoring with Strong Trace Prefixes
mechanized proof	(Recorded) End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT
message-passing	Collective Contracts for Message-Passing Parallel Programs
MIP	Arithmetic Solving in Z3
model based projection	Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement
Model checker	(Distinguished Paper) (Recorded) Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games
model checking	Optimization-Based Model Checking for Complex STL Specifications Avoiding the Shoals - A New Approach to Liveness Checking Compositional Value Iteration with Pareto Caching (Recorded) Measurement-based Verification of Quantum Markov Chains Testing the migration from analog to software-based Railway Interlocking Systems
model-based testing	Testing the migration from analog to software-based Railway Interlocking Systems
model-checking	Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
Monitoring	General Anticipatory Runtime Verification Monitizer: Automating Design and Evaluation of Neural Network Monitors
monotone	(Recorded) Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates
MPI	Collective Contracts for Message-Passing Parallel Programs
multi-objective optimization	Compositional Value Iteration with Pareto Caching
Multi-path loops	On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches
mypyvy	mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
N
Neural Barrier Certificates	Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
Neural Network Verification	Boosting Few-Pixel Robustness Verification via Covering Verification Designs Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Neural Networks	(Recorded) Verifying Global Two-Safety Properties in Neural Networks with Confidence Monitizer: Automating Design and Evaluation of Neural Network Monitors
NLP	How to Solve Math Problems without Talent
nonlinear arithmetic	(Recorded) Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates
Nonlinear invariant generation	On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches
Nonlinear systems	(Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
O
Obligations	Proactive Real-Time First-Order Enforcement
Omega-Automata	Synthesis of Temporal Causality
Online verification	Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems
opening	Opening Remarks
Operator Precedence Languages	SMT-based Symbolic Model-Checking for Operator Precedence Languages
optimization	Optimization-Based Model Checking for Complex STL Specifications
oracle guided synthesis	Guiding Enumerative Program Synthesis with Large Language Models
P
Parallel Computing	(Distinguished Paper) (Recorded) Distributed SMT Solving Based on Dynamic Variable-level Partitioning
Partial exploration	(Distinguished Paper) (Recorded) Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games
Partial Observability	What should be observed for optimal reward in POMDPs?
Partial Order Reduction	Parsimonious Optimal Dynamic Partial Order Reduction
Partitioning Strategy	(Distinguished Paper) (Recorded) Distributed SMT Solving Based on Dynamic Variable-level Partitioning
permission-based separation logic	The VerCors Verifier: a Progress Report
polynomial ranking functions	(Recorded) Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates
POMDPs	What should be observed for optimal reward in POMDPs?
portfolio	Verification Algorithms for Automated Separation Logic Verifiers
prediction	Predictive Monitoring with Strong Trace Prefixes
Presburger arithmetic	Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic Strided Difference Bound Matrices
Probabilistic model checking	Stochastic Omega-Regular Verification and Control with Supermartingales What should be observed for optimal reward in POMDPs?
probabilistic programs	Lexicographic Ranking Supermartingales with Lazy Lower Bounds
probabilistic system	Compositional Value Iteration with Pareto Caching
Probabilistic verification	(Distinguished Paper) (Recorded) Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games
probability theory	(Recorded) Probabilistic Access Policies with Automated Reasoning Support
Program repair	Syntax-Guided Automated Program Repair For Hyperproperties
Program Synthesis	Guiding Enumerative Program Synthesis with Large Language Models LTL learning on GPUs
Program Verification	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
proof assistant	Lean 4: Bridging Formal Mathematics and Software Verification
proof certification	(Distinguished Paper) Formally Certified Approximate Model Counting
Proof Debugging	(Distinguished Paper) A Framework for Debugging Automated Program Verification Proofs via Proof Actions
Propositional Proofs	CaDiCaL 2.0
Q
quantifier alternation	Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
Quantifiers	Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement
Quantum circuit simulation	Simulating Quantum Circuits by Model Counting
Quantum Computing	Simulating Quantum Circuits by Model Counting
Quantum Markov chain	QReach: A Reachability Analysis Tool for Quantum Markov Chains
Quantum Markov chains	(Recorded) Measurement-based Verification of Quantum Markov Chains
Quantum Model Checking	QReach: A Reachability Analysis Tool for Quantum Markov Chains
Quantum Programming Languages	Approximate Relational Reasoning for Quantum Programs
Quantum Walks	(Recorded) Measurement-based Verification of Quantum Markov Chains
R
railway interlockings systems	Testing the migration from analog to software-based Railway Interlocking Systems
randomized algorithms	(Distinguished Paper) Formally Certified Approximate Model Counting
ranking function synthesis	(Recorded) Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates
ranking supermartingale	Lexicographic Ranking Supermartingales with Lazy Lower Bounds
Reachability Analysis	(Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis QReach: A Reachability Analysis Tool for Quantum Markov Chains
reactive synthesis	Localized Attractor Computations for Infinite-State Games
Reactive Systems	Synthesis of Temporal Causality
Reactive verification	Bisimulation Learning
Reconfigurable	(Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
Recurrence analysis	On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches
recursion	Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automaton
regular languages	(Distinguished Paper) Regular Reinforcement Learning
regular model checking	(Distinguished Paper) Regular Reinforcement Learning
Reinforcement Learning	Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models (Distinguished Paper) Regular Reinforcement Learning
Relational Hoare Logic	Approximate Relational Reasoning for Quantum Programs
relational synthesis	Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automaton
relay-based circuits	Testing the migration from analog to software-based Railway Interlocking Systems
remarks	Opening Remarks
robustness verification	Certified Robust Accuracy of Neural Networks Are Bounded due to Bayes Errors
Runtime enforcement	Proactive Real-Time First-Order Enforcement
Runtime Verification	General Anticipatory Runtime Verification Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
S
Safe Exploration	Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models
Safety Verification	Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
SAT	Arithmetic Solving in Z3 CaDiCaL 2.0
SAT solving	From Clauses to Klauses
Satisfiability	Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement Simulating Quantum Circuits by Model Counting CaDiCaL 2.0
Satisfiability Modulo Theories	(Distinguished Paper) (Recorded) Distributed SMT Solving Based on Dynamic Variable-level Partitioning
separation logic	Verification Algorithms for Automated Separation Logic Verifiers
Set-boundary analysis	(Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
Smart Contract Verification	(Recorded) hevm, a Fast Symbolic Execution Framework for EVM Bytecode
SMT	Scalable Bit-Blasting with Abstractions Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement Split Gröbner Bases for Satisfiability Modulo Finite Fields Arithmetic Solving in Z3 SMLP: Symbolic Machine Learning Prover Symbolic Model-Checking Intermediate-Language Tool Suite
SMT encoding	(Recorded) Probabilistic Access Policies with Automated Reasoning Support
SMT solver	Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic Verification Algorithms for Automated Separation Logic Verifiers
smt solving	soid: A Tool for Legal Accountability for Automated Decision Making (Distinguished Paper) (Recorded) Interactive Theorem Proving modulo Fuzzing
SMT-based Model Checking	SMT-based Symbolic Model-Checking for Operator Precedence Languages
Software model checking	Bisimulation Learning
software verification	Lean 4: Bridging Formal Mathematics and Software Verification
Solidity Smart Contracts	SolTG: A CHC-based Solidity Test Case Generator
specification	Optimization-Based Model Checking for Complex STL Specifications LTL learning on GPUs
Specification Language	Symbolic Model-Checking Intermediate-Language Tool Suite
Specification Synthesis	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Stability	SMLP: Symbolic Machine Learning Prover
Stabilizer Formalism	Simulating Quantum Circuits by Model Counting
Stateless Model Checking	Parsimonious Optimal Dynamic Partial Order Reduction
Static analysis	The Top-Down Solver Verified: Building Confidence in Static Analyzers Strided Difference Bound Matrices
Stochastic control synthesis	Stochastic Omega-Regular Verification and Control with Supermartingales
Stochastic games	(Distinguished Paper) (Recorded) Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games
strategy improvement	Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement
Stream Monitoring	Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
Stutter-insensitive bisimulation	Bisimulation Learning
Sub-polyhedral abstract domain	Strided Difference Bound Matrices
SyGuS	Syntax-Guided Automated Program Repair For Hyperproperties
Symbol Model Checking	Symbolic Model-Checking Intermediate-Language Tool Suite
symbolic abstraction	Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
Symbolic Execution	Verification Algorithms for Automated Separation Logic Verifiers SolTG: A CHC-based Solidity Test Case Generator (Recorded) hevm, a Fast Symbolic Execution Framework for EVM Bytecode
Symbolic Reasoning	General Anticipatory Runtime Verification
syntax guided synthesis	Guiding Enumerative Program Synthesis with Large Language Models
SYNTCOMP	The Reactive Synthesis Competition (SYNTCOMP) Report
Synthesis	Synthesis of Temporal Causality The SemGuS Toolkit The Reactive Synthesis Competition (SYNTCOMP) Report
System Optimization	SMLP: Symbolic Machine Learning Prover
Sādhak	(Distinguished Paper) (Recorded) Interactive Theorem Proving modulo Fuzzing
T
temporal logic	Optimization-Based Model Checking for Complex STL Specifications Proactive Real-Time First-Order Enforcement SMT-based Symbolic Model-Checking for Operator Precedence Languages
termination	(Recorded) Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates
Testing	Parsimonious Optimal Dynamic Partial Order Reduction
theorem proving	Lean 4: Bridging Formal Mathematics and Software Verification
theory of linear integer/real rings	(Recorded) Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates
Trace	LTL learning on GPUs
Trace Analysis	LTL learning on GPUs
trace theory	Predictive Monitoring with Strong Trace Prefixes
Transparency	Syntax-Guided Automated Program Repair For Hyperproperties
Tree-shaped Tableau	SMT-based Symbolic Model-Checking for Operator Precedence Languages
Type system	Verifying Cake Cutting, Faster
U
uncertainty	(Recorded) Probabilistic Access Policies with Automated Reasoning Support
V
value iteration	Compositional Value Iteration with Pareto Caching
Verification	Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models Collective Contracts for Message-Passing Parallel Programs (Recorded) Verifying Global Two-Safety Properties in Neural Networks with Confidence
verification condition generation	Verification Algorithms for Automated Separation Logic Verifiers
Verification Engineering	(Distinguished Paper) A Framework for Debugging Automated Program Verification Proofs via Proof Actions
virtual machines	(Recorded) End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT
W
Weakly relational abstract domains	Strided Difference Bound Matrices
Weighted Model Counting	Simulating Quantum Circuits by Model Counting
Z
Zero-Knowledge Proofs	Split Gröbner Bases for Satisfiability Modulo Finite Fields
Zonotopal tiling	(Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
ω
ω-regular verification	Stochastic Omega-Regular Verification and Control with Supermartingales

Disclaimer | Powered by EasyChair Smart Program