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.
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
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 Session 2 (9:20 - 10:20) - Concurrency + Misc
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 Day 2 - July 21
Session 1A (8:30 - 9:00) - Synthesis + Probabilistic/statistical Techniques 2
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 Session 2A (8:30 - 9:00) - Complexity and Termination
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 Session 1B (9:20 - 10:20) - Decision Procedures and Solvers
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 Session 2B (9:20 - 10:20) - Hybrid and Cyber Physical Systems
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 Day 3 - July 22
Session 1A (9:20 - 10:20) - Synthesis + Probabilistic/statistical Techniques 1
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 Session 2A (9:20 - 10:20) - Model Checking
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 Session 1B (10:30 - 11:00) - Logical Foundations
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 Session 2B (10:30 - 11:00) - Software Verification 2
note 2nd block is one day later on day 4
Session 1A (9:20 - 10:20) - Security + Misc
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 Session 2A (9:20 - 10:20) - Software Verification 1
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