| 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.30am | SW 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.30pm | Invited 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 |
| Closing | |