Monday 20th July
8.30am–10.30am Opening
Tutorial 1
Joost-Pieter Katoen
The What, Why and How of Probabilistic Verification
10.30am–11.00am Coffee Break
11.00am–12.00pm Tutorial 1 cont.
12.00pm–1.30pm Lunch
1.30pm–3.30pm Tutorial 2
Madhusudan Parthasarathy and Pranav Garg
Machine-learning based methods for synthesizing invariants
3.30pm–4.00pm Coffee Break
4.00pm–5.40pm Tutorial 2 cont.
6.30pm Reception - B Restaurant

Tuesday 21st July
8.30am–10.30am Model Checking and Refinement
Session Chair — Natasha Sharygina

Cook, Khlaaf and Piterman. On Automation of CTL* Verification for Infinite-State Systems

Finkbeiner, Rabe and Sanchez. Algorithms for Model Checking HyperLTL and HyperCTL*

Dietsch, Heizmann, Langenfeld and Podelski. Fairness Modulo Theory: A New Approach to LTL Software Model Checking

Durand-Gasselin, Esparza, Ganty and Majumdar. Model Checking Parameterized Asynchronous Shared-Memory Systems

Konnov, Veith and Widder. SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms

Manolios and Jain. Skipping Refinement

10.30am–11.00am Coffee Break
11.00am–12.00pm Invited Talk: Leslie Lamport — What Should Math Have to do with Building Complex Distributed Systems?
12.00pm–1.30pm Lunch
1.30pm–3.30pm Quantitative Reasoning
Session Chair — Joost-Pieter Katoen

Randour, Raskin and Sankur. Percentile Queries in Multi-Dimensional Markov Decision Processes

Chatterjee, Ibsen-Jensen and Pavlogiannis. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs

Brazdil, Chatterjee, Chmelík, Fellner and Kretinsky. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes

Gleissenthall, Köpf and Rybalchenko. Symbolic Polytopes for Quantitative Interpolation and Verification

Abate, Ceska, Brim and Kwiatkowska. Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks

Dehnert, Junges, Jansen, Corzilius, Volk, Bruintjes, Katoen and Abraham. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool

3.30pm–4.00pm Coffee Break
4.00pm–5.40pm SW Analysis I
Session Chair — Aws Albarghouthi

Zheng, Ganesh, Subramanian, Tripp, Dolby and Zhang. Effective Search-space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints

Aydin, Bang and Bultan. Automata-based Model Counting for String Constraints

Gouw, Rot, De Boer, Bubel and Haehnle. OpenJDK's java.utils.Collection.sort() is broken: The Good, the Bad and the Worst Case

Grigore and Kiefer. Tree Buffers

Gehr, Dimitrov and Vechev. Learning Commutativity Specifications

7.00pm PC Dinner

Wednesday 22nd July
8.30am–10.30amSW Analysis II
Session Chair — Domagoj Babic

Das, Lahiri, Lal and Li. Angelic Verification: Precise Verification Modulo Unknowns

Kahsai, Navas, Gurfinkel and Komuravelli. The SeaHorn Verification Framework

Lahiri, Sinha and Hawblitzel. Automatic Rootcausing for Program Equivalence Failures in Binaries

Leino and Wuüstholz. Fine-grained Caching of Verification Results

Singh and Gulwani. Predicting a Correct Program in Programming By Example

Oulamara and Venet. Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation

10.30am–11.00am Coffee Break
11.00am–12.00pm Invited Talk: Philippa Gardner
A Trusted Mechanised Specification of JavaScript: One Year On
12.00pm–1.30pm Lunch
1.30pm–2.00pm CAV Award
Session Chair — Corina Pasareanu
2.00pm–3.00pm Competitions and Artifact Evaluation
Session Chair — Corina Pasareanu
3.00pm–3.30pm Lightning Talks I
Session Chair — Corina Pasareanu

Finkbeiner, Gieseking and Olderog. ADAM: Causality-Based Synthesis of Distributed Systems

Saha, Garg and Parthasarathy. Alchemist: Learning Guarded Affine Functions

Sebastiani and Trentin. OptiMathSAT: A Tool for Optimization Modulo Theories

Kulahcioglu, Emmi and Tasiran. Systematic Asynchrony Bug Exploration for Android Apps

Abdulla, Atig, Holik, Ruemmer, Stenman, Rezine and Chen. Norn: a solver for string constraints

Masci, Oladimeji, Zhang, Jones, Curzon and Thimbleby. PVSio-web 2.0: Joining PVS to Human-Computer Interaction

3.30pm–4.00pm Coffee Break
4.00pm-5.40pm Interpolation, IC3/PDR, and Invariants
Session Chair — Orna Grumberg

Karbyshev, Bjorner, Itzhaky, Rinetzky and Shoham. Property-Directed Inference of Universal Invariants or Proving Their Absence

Bozzano, Cimatti, Griggio and Mattarei. Efficient Anytime Techniques for Model-Based Safety Analysis

Beyer, Dangl and Wendler. Boosting k-Induction with Continuously-Refined Invariants

Vizel, Gurfinkel and Malik. Fast Interpolating BMC

Chen, Hong, Wang and Zhang. Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation

6.00pm Business meeting
8.00pm Banquet and Poster Session in Conference Hotel

Thursday 23rd July — Industry Day
8.30am–10.30am SMT techniques and applications
Session Chair — Ofer Strichman

Zhu, Petri and Jagannathan. Poling: SMT Aided Linearizability Proofs

Erez and Nadel. Finding Bounded Path in Graph using SMT for Automatic Clock Routing

Christ and Hoenicke. Cutting the Mix

Manolios, Papavasileiou and Pais. The Inez Mathematical Programming Modulo Theories Framework

Bacchus and Katsirelos. Using Minimal Correction Sets to more Efficiently compute Minimal Unsatisfiable Sets

Bansal, Reynolds, King, Barrett and Wies. Deciding Local Theory Extensions via E-matching

10.30am–11.00am Coffee Break
11.00am–12.00pm Invited Talk: Bob Kurshan — CAV: An Industrial Perspective
12.00pm–1.30pm Lunch
1.30pm–2.30pmInvited Talk: William Hung — Effective and Scalable Verification: Bridging Research HW Verification
2.30pm – 3.30pm Hardware
Session Chair — Daniel Kroening

Vijayaraghavan, Chlipala, Arvind and Dave. Modular Deductive Verification of Multiprocessor Hardware Designs

Chakraborty, Khasidashvili, Seger, Gajavelly, Haldankar, Chhatani and Mistry. Word-level Symbolic Trajectory Evaluation

Leslie-Hurd, Caspi and Fernandez. Verifying Linearizability of Intel Software Guard Extensions

3.30pm–4.00pm Coffee Break
4.00pm–4.30pm Lightning Talks II
Session Chair — Zvonimir Rakamaric

Babiak, Blahoudek, Duret-Lutz, Klein, Křetínský, Müller, Parker and Strejcek. The Hanoi Omega-Automata Format

Isberner, Howar and Steffen. The Open-Source LearnLib: A Framework for Active Automata Learning

Majumdar and Wang. BBS: A Phase-Bounded Model Checker for Asynchronous Programs

Tiwari. Time-Aware Abstractions in HybridSal

Reinking and Piskac. A Type-Directed Approach to Program Repair

4.30pm–5.50pm Case Studies and Empirical Metrics
Session Chair — Zvonimir Rakamaric

Bozzano, Cimatti, Pires, Jones, Kimberly, Petri, Robinson and Tonetta. Formal Design and Safety Analysis of AIR6110 Wheel Brake System

Duggirala, Fan, Mitra and Viswanathan. Meeting a Powertrain Verification Challenge

Woodhouse, Piterman, Köksal and Fisher. Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data

Demyanova, Pani, Veith and Zuleger. Empirical Software Metrics for Bench- marking of Verification Tools

6.30pm Excursion to Exploratorium

Friday 24th July
8.30am–10.30am Synthesis
Session Chair — Ahmed Bouajjani

Alur, Cerny and Radhakrishna. Synthesis through Unification

Cerny, Clarke, Henzinger, Radhakrishna, Ryzhyk, Samanta and Tarrach. From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis

Reynolds, Deters, Kuncak, Tinelli and Barrett. Counter-example Guided Quantifier Instantiation for Synthesis in SMT

Kneuss, Koukoutos and Kuncak. Deductive Program Repair

Deshmukh, Majumdar and Prabhu. Quantifying System Conformance using the Skorokhod Metric

Brenguier and Raskin. Pareto Curves of Multidimensional Mean-Payoff Games

10.30am–11.00am Coffee Break
11.00am–12.00pm Invited Talk: Peter O'Hearn
12.00pm–1.30pm Lunch
1.30pm–2.30pm Termination
Session Chair — Arie Gurfinkel

D'Silva and Urban. Conflict Driven Conditional Termination

Kuwahara, Sato, Unno and Kobayashi. Predicate Abstraction and CEGAR for Disproving Termination of Higher-order Functional Programs

Ben-Amram and Genaim. Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions

2.30pm–3.30pm Analysis of Hybrid Systems and Quantitative Reasoning
Session Chair — Arie Gurfinkel

Ferrere, Maler, Nickovic and Ulus. Measuring with Timed Patterns

Zou, Fränzle, Zhan and Mosaad. Automatic Stability and Safety Verification for Delay Differential Equations

Akazaki and Hasuo. Time Robustness in MTL and Expressivity in Hybrid System Falsification

3.30pm–4.00pm Coffee Break
4.00pm–5.40pm Concurrency
Session Chair — Kedar Namjoshi

Jeon, Qiu, Solar-Lezama and Foster. Adaptive Concretization for Parallel Program Synthesis

Alur, Raghothaman, Stergiou, Tripakis and Udupa. Automatic Completion of Distributed Protocols with Symmetry

Mansky, Garbuzov and Zdancewic. An Axiomatic Specification for Sequential Memory Models

Desai, Seshia, Qadeer, Broman and Eidson. Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems

Hawblitzel, Petrank, Qadeer and Tasiran. Automated and modular refinement reasoning for concurrent programs