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.

Day 1 - July 20

Session 1 (9:20 - 10:20) - AI

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

Session 2 (9:20 - 10:20) - Concurrency + Misc

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

Day 2 - July 21

Session 1A (8:30 - 9:00) - Synthesis + Probabilistic/statistical Techniques 2

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

Session 2A (8:30 - 9:00) - Complexity and Termination

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

Session 1B (9:20 - 10:20) - Decision Procedures and Solvers

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

Session 2B (9:20 - 10:20) - Hybrid and Cyber Physical Systems

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

Day 3 - July 22

Session 1A (9:20 - 10:20) - Synthesis + Probabilistic/statistical Techniques 1

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

Session 2A (9:20 - 10:20) - Model Checking

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

Session 1B (10:30 - 11:00) - Logical Foundations

note 2nd block is one day later on day 4
73Porous Invariants
201Learning Union of Integer Hypercubes with Queries (with applications to monadic decomposition)
1Towards a Trustworthy Semantics-Based Language Framework via Proof Generation
12Formal Foundations of Fine-Grained Explainability

Session 2B (10:30 - 11:00) - Software Verification 2

note 2nd block is one day later on day 4
188Gillian, Part II: Real-World Verification for JavaScript and C
215Debugging Network Reachability with Blocked Paths
288Fast Computation of Strong Control Dependencies
311Diffy: Inductive Reasoning of Array Programs using Difference Invariants

Day 4 - July 23

Session 1A (9:20 - 10:20) - Security + Misc

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

Session 2A (9:20 - 10:20) - Software Verification 1

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