CAV Paper Schedule

This page is a dynamic version of the content here: CAV'21 Attending

This site was set up quickly to assist authors when the schedule was initially released. This page will not be update in case of last minute changes.

The conference mini-site is now the most reliable source of information (and supports time-zone selection): find the schedule here.

Select your timezone (we've made a guess).
The schedule shows the start time of each block in the 'CAV choice time zone' followed by your timezone.

ID	Paper Title
65	DNNV: A Framework for Deep Neural Network Verification
83	Robustness Verification of Quantum Classifiers
88	BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks
115	Automated Safety Verification of Programs Invoking Neural Networks
187	Scalable Polyhedral Verification of Recurrent Neural Networks
190	Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning
225	Robustness Verification of Semantic Segmentation Neural Networks using Relaxed Reachability
259	PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier

158	Ghost Signals: Verifying Termination of Busy Waiting
41	Isla: Integrating full-scale ISA semantics and axiomatic concurrency models
178	Stateless Model Checking under a Reads-Value-From Equivalence
186	Gobra: Modular Specification and Verification of Go Programs
189	Delay-Bounded Scheduling Without Delay!
195	Checking Data-Race Freedom of GPU Kernels, Compositionally
313	GenMC: A Model Checker for Weak Memory Models
62	Summing Up Smart Transitions

180	Adapting Behaviors via Reactive Synthesis
284	Causality-based Game Solving
224	Rigorous Floating-Point Roundoff Error Analysis of Probabilistic Computations
293	Model-free Reinforcement Learning for Branching Markov Decision Processes

238	Reflections on Termination of Linear Loops
240	Decision Tree Learning in CEGIS-Based Termination Analysis
294	ATLAS: Automated Amortised Complexity Analysis of Self-Adjusting Data Structures
262	Lower-Bound Synthesis using Loop Specialization and Max-SMT

47	Theory Exploration Powered by Deductive Synthesis
55	CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver
100	JavaSMT 3: Interacting with SMT Solvers in Java
177	Efficient SMT-based Analysis of Failure Propagation
193	ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends
209	Interpolation and Model Checking for Nonlinear Arithmetic
220	An SMT Solver for Regular Expressions and Linear Arithmetic over String Length
298	Counting Minimal Unsatisfiable Subsets

116	Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
131	An Iterative Scheme of Safe Reinforcement Learning for Nonlinear Systems via Barrier Certificate Generation
148	HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous CPSs in AADL
164	Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems
171	IMITATOR 3: Synthesis of timing parameters beyond decidability
264	SceneChecker: Boosting Scenario Verification using Symmetry Abstractions
304	Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness
324	Fast zone-based algorithms for reachability in pushdown timed automata

48	Synthesis with Asymptotic Resource Bounds
75	Program Sketching by Automatically Generating Mocks from Tests
150	Counterexample-Guided Partial Bounding for Recursive Function Synthesis
172	PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs
167	Latticed k-Induction with an Application to Probabilistic Programs
102	Learning Probabilistic Termination Proofs
81	Runtime Monitors for Markov Decision Processes
197	Enforcing Almost-Sure Reachability in POMDPs

306	Sound Verification Procedures for Temporal Properties of Infinite-State Systems
40	Progress in Certifying Hardware Model Checking Results
66	Model-Checking Structured Context-Free Languages
113	Model Checking ω-Regular Properties with Decoupled Search
144	AIGEN: Random Generation of Symbolic Transition Systems
182	GPU Acceleration of Bounded Model Checking with ParaFROST
212	Pono: A Flexible and Extensible SMT-based Model Checker
86	Model Checking Finite-Horizon Markov Chains with Probabilistic Inference

note 2nd block is one day later on day 4

73	Porous Invariants
201	Learning Union of Integer Hypercubes with Queries (with applications to monadic decomposition)
1	Towards a Trustworthy Semantics-Based Language Framework via Proof Generation
12	Formal Foundations of Fine-Grained Explainability

note 2nd block is one day later on day 4

188	Gillian, Part II: Real-World Verification for JavaScript and C
215	Debugging Network Reachability with Blocked Paths
288	Fast Computation of Strong Control Dependencies
311	Diffy: Inductive Reasoning of Array Programs using Difference Invariants

46	Verified Cryptographic Code for Everybody
56	Not All Bugs Are Created Equal, But Robust Reachability Can Tell The Difference
161	A Temporal Logic for Asynchronous Hyperproperties
203	Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security
226	Constraint-based Relational Verification
315	Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning
163	Computing Bottom SCCs Symbolically Using Transition Guided Reduction
207	Formally Verified Switching Logic for Recoverability of Aircraft Controller

14	Cameleer: a Deductive Verification Tool for OCaml
64	LLMC: Verifying High-Performance Software
93	Formally Validating a Practical Verification Condition Generator
95	Automatic Generation and Validation of Instruction Encoders and Decoders
107	An SMT Encoding of LLVM’s Memory Model for Bounded Translation Validation
112	Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios
154	Functional Correctness of C implementations of Dijkstra’s, Kruskal’s, and Prim’s Algorithms