Registration

Registration is now open. Register for CAV’21 here.
Early registration is possible until July 9 2021, with regular registration being possible up to the conference. The registration fees for students are really low ($10-$30) and we offer NSF-funded fellowships for US students (application deadline is July 2). We hope this will encourage many students to join us this year at CAV.
We are looking forward to seeing you at CAV 2021!

Participating in CAV’21

Note: After the conference, the CAV’21 conference page (cav21.org) has been made public and is accessible here without any registration.

If you have registered for CAV’21, an account has been created for you at cav21.org. It uses the email address you registered with. Please activate this account so you have access to the conference page as well as to the cav21 slack workspace and our gather. Make sure to read the Getting Started paragraph on cav21.org to learn more and find the links to slack and gather.

On cav21.org, you will find the relevant information for all events at CAV’21, including the zoom links. If you have any questions, feel free to ask in the helpdesk channel on slack (or send an email to support@cav21.org if you have trouble joining us there). Note that the slack workspace and the support address are not maintained anymore after the conference.

Virtual Conference Format

Please be aware that the following information is tentative and might change again.

Dates and Times: CAV will take place online Sunday July 18th – Saturday July 24th, with the main conference on Tuesday-Friday. Every day will be 4h of activities, 8am-12pm PDT (which is 4-8pm UK time). We will be mirroring the schedule 11 hours later at 8am-12pm in GMT+6 (which is 7-11pm PDT and 3-7am UK time), to enable wider participation of colleagues in Asia/Australia time zones. Workshops might follow a different schedule, information can be found on their websites.

Communication channels: We will be using Slack for (asynchronous) communication and discussions on papers and Gather for interactions with our sponsors and social events – join us for the pub quiz!

Program: We will have a virtual conference website which will contain the schedule and all relevant links. You can find the (tentative) publicly accessible schedule here, other parts of the page are only accessible to CAV attendees.

Presentations: Each paper will have a 5min talk and a 25min talk. The 5min talk will be streamed during the conference and the 25min talk will be available before and after the conference for people to watch. So make sure to check out the talks already during the week before CAV!

Watch Parties: Feel free to organize (safe) watch parties with your fellow researchers and friends and let us know on social media (#cav21).

CAV Paper Sessions

Every session will be held twice: Once during the first block (8am-12pm PDT, 4-8pm UK time, 9pm-1am GMT+6) and then again in the second block 11 hours later (7-11pm PDT, 3-7am UK time, 8am-12pm GMT+6). Note that CAV will have parallel sessions. The following schedule is tentative and might change until the conference.

We give one day and time per session. For the first block, this is the time in PDT on that day. For the second block, this is the time in GMT+6 on the following day. As an example, a session given with 8-9 on July 20 will happen once at 8-9am PDT (which is 4-5pm UK time and 9-10pm GMT+6) and will be repeated at 8-9am on July 21 GMT+6 (which is 7-8pm on July 20 PDT and 3-4am on July 21 UK time). David Purser created a dynamic version of the following schedule that displays the times in your selected time zone, you can find it here.

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
only in the first block, repeated 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
only in the first block, repeated 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

Day 4 – July 23

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

Session 1B (10:30 – 11:00) – Logical Foundations
only in the second block, repeated session from Day 3

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
only in the second block, repeated session from Day 3

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

Virtualization Committee

Tiago Ferreira, University College London (chair)
Laura Graves, University of Waterloo
Adharsh Kamath, NITK, Surathkal
Hanneli Tavante, McGill University
Justin Wong, UC Berkeley