Program

The conference proceedings are available:
Computer Aided Verification29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I
Computer Aided Verification29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II

The workshops (except David Dill @ 60 Workshop) happen at the Hotel Crowne Plaza.

Room Animus 1 Animus 2 Terra Natura Lux
22 July SYNT NSV / Rise4CPS SMT VSTTE DARS
23 July VMW NSV / Rise4CPS SMT VSTTE FEVER

The main conference (and David Dill @ 60 Workshop) happen at the Heidelberg Stadthalle.

Monday 24th July, Stadthalle
09:00 – 10:00 David Dill @ 60 Workshop Session 1
10:00 – 10:30 Coffee Break
10:30 – 12:00 David Dill @ 60 Workshop Session 2
In the afternoon, the workshop continues and stays in Stadthalle, but moves to an adjacent Ball Room to make space for CAV tutorials to which it runs in parallel.
13:30 – 15:00 Tutorial. Chair: Thomas WahlThe Power of Symbolic Automata and Transducers.Loris D’Antoni.
15:00 – 16:00 Coffee break
– 17:30 Tutorial. Chair: Georg WeissenbacherMaximum Satisfiability in Software Analysis: Applications and TechniquesMayur Naik.
18:00 Reception in Stadthalle

Talks for regular CAV papers are 20 minutes including questions and set-up times.
Talks for CAV tool papers are 10 minutes including questions and set-up times.

Tuesday 25th July, Stadthalle
8:45 – 9:00 Welcome by Conference Program Chairs
09:00 – 10:00 Invited Talk. Chair: Viktor KuncakFast Verification of Fast Cryptography for Secure SocketsChris Hawblitzel.
10:00 – 10:30 Coffee break
10:30 – 12:30 Probabilistic Systems. Chair: Hana Chockler
10:30 – 10:50 Reluplex: An Efficient SMT Solver for Verifying Deep Neural NetworksGuy Katz, Clark Barrett, David Dill, Kyle Julian, Mykel Kochenderfer.
10:50 – 11:10 Automated Recurrence Analysis for Almost-Linear Expected-Runtime BoundsKrishnendu Chatterjee, Hongfei Fu, Aniket Murhekar.
11:10 – 11:30 Markov Automata with Multiple ObjectivesTim Quatmann, Sebastian Junges, Joost-Pieter Katoen.
11:30 – 11:50 Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision ProcessesChristel Baier, Joachim Klein, Linda Leuschner, David Parker, Sascha Wunderlich.
11:50 – 12:10 Repairing Decision-Making Programs under UncertaintyAws Albarghouthi, Loris D’Antoni, Samuel Drews.
12:10 – 12:30 Value Iteration for Long-run Average Reward in Markov Decision ProcessesPranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Křetínský, Tobias Meggendorfer.
12:30 – 14:00 Lunch
14:00 – 15:30 Data Driven Techniques. Chair: Daniel Kroening
14:00 – 14:10 STLInspector: STL Validation with GuaranteesHendrik Röhm, Thomas Heinz, Eva Charlotte Mayer [Tool paper].
14:10 – 14:30 Learning a Static Analyzer from DataPavol Bielik, Veselin Raychev, Martin Vechev.
14:30 – 14:50 Synthesis with Abstract ExamplesDana Drachsler Cohen, Sharon Shoham, Eran Yahav.
14:50 – 15:10 Data-Driven Synthesis of Full Probabilistic ProgramsSarah Chasins, Phitchaya Mangpo Phothilimthana.
15:10 – 15:30 Logical Clustering and Learning for Time-Series DataMarcell Vazquez-Chanlatte, Jyotirmoy Deshmukh, Xiaoqing Jin, Sanjit A. Seshia.
15:30 – 15:40 Results of Synthesis CompetitionsDana Fisman, Swen Jacobs
15:40 – 16:00 Coffee break
16:00 – 17:30 Runtime Verification and New Applications. Chair: Anna Slobodova
16:00 – 16:10 Montre: A Tool for Monitoring Timed Regular ExpressionsDogan Ulus [Tool paper].
16:10 – 16:30 Runtime Monitoring with Recovery of the SENT Communication ProtocolKonstantin Selyunin, Stefan Jaksic, Thang Nguyen, Christian Reidl, Udo Hafner, Ezio Bartocci, Dejan Nickovic, Radu Grosu.
16:30 – 16:50 Runtime Verification of Temporal Properties over Out-of-order Data StreamsDavid Basin, Felix Klaedtke, Eugen Zalinescu.
16:50 – 17:10 Verified compilation of space-efficient reversible circuitsMatthew Amy, Martin Roetteler, Krysta Svore.
17:10 – 17:30 Ascertaining Uncertainty for Efficient Exact Cache AnalysisClaire Maiza, David Monniaux, Jan Reineke, Valentin Touzeau.
Wednesday 26th July, Stadthalle
09:00 – 10:00 Invited Talk. Chair: Aarti GuptaSafety Verification of Deep Neural NetworksMarta Kwiatkowska.
10:00 – 10:30 Coffee break
10:30 – 12:30 Cyber-physical Systems. Chair: Pavithra Prabhakar
10:30 – 10:50 Lagrangian ReachabililtyJacek Cyranka, Md Ariful Islam, Greg Byrne, Paul L. Jones, Scott A. Smolka, Radu Grosu.
10:50 – 11:10 Simulation-Equivalent Reachability of Large Linear Systems with InputsStanley Bak, Parasara Sridhar Duggirala.
11:10 – 11:30 MightyL: A Compositional Translation from MITL to Timed AutomataThomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege.
11:30 – 11:50 DryVR: Data-driven verification and compositional reasoning for automotive systemsChuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan.
11:50 – 12:10 Automated Formal Synthesis of Digital Controllers for State-Space Physical PlantsAlessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen.
12:10 – 12:30 Classification and coverage-based falsification for embedded control systemsArvind S Adimoolam, Thao Dang, Alexandre Donze, James Kapinski, Xiaoqing Jin.
12:30 – 14:00 Lunch
14:00 – 15:30 Concurrency. Chair: Andrey Rybalchenko
14:00 – 14:20 GPUDrano: Detecting Uncoalesced Accesses in GPU ProgramsRajeev Alur, Joseph Devietti, Omar S. Navarro Leija, Nimit Singhania.
14:20 – 14:40 Context-Sensitive Dynamic Partial Order ReductionElvira Albert, Puri Arenas, Maria Garcia de la Banda, Miguel Gomez-Zamalloa, Peter Stuckey.
14:40 – 15:00 Starling: Lightweight Concurrency Verification With ViewsMatthew Windsor, Mike Dodds, Matthew J Parkinson, Ben Simner.
15:00 – 15:20 Compositional Model Checking with Incremental Counter-Example ConstructionAnton Wijs, Thomas Neele.
15:20 – 15:30 Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-Affine Dynamical SystemsNikola Beneš, Luboš Brim, Martin Demko, Samuel Pastva, David Šafránek [Tool paper].
15:30 – 16:00 Coffee break
16:00 – 17:30 Analysis of Software and Hardware. Chair: Zvonimir Rakamaric
16:00 – 16:20 Non-polynomial Worst-Case Analysis of Recursive ProgramsKrishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady.
Automated Resource Analysis with Coq Proof Objects16:20 – 16:40 Quentin Carbonneaux, Jan Hoffmann, Thomas Reps, Zhong Shao.
16:40 – 17:00 Look for the Proof to Find the Program: Decorated-Component-Based Program SynthesisAdria Gascon, Ashish Tiwari, Brent Carmer, Umang Mathur.
17:00 – 17:20 E-QED: Electrical Bug Localization During Post-Silicon Validation Enabled by Quick Error Detection and Formal MethodsEshan Singh, Clark Barrett, Subhasish Mitra.
17:20 – 17:30 SMTCoq: A plug-in for integrating SMT solvers into CoqBurak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark Barrett [Tool paper].
17:30 Business Meeting
Thursday 27th July, Stadthalle
09:00 – 10:00 Winner of the CAV Award. CAV Award Talk.
Chair: Orna Grumberg
10:00 – 10:30 Coffee break
10:30 – 12:30 Foundations. Chair: Wei-Ngan Chin
10:30 – 10:50 Efficient Parallel Strategy Improvement for Parity GamesJohn Fearnley.
10:50 – 11:10 Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systemsMarie Fortin, Anca Muscholl, Igor Walukiewicz.
11:10 – 11:30 Minimization of Symbolic TransducersOlli Saarikivi, Margus Veanes.
11:30 – 11:50 Abstract Interpretation with Unfoldings Marcelo Sousa, César Rodríguez, Vijay D’Silva, Daniel Kroening.
11:50 – 12:10 Cutoff Bounds for Consensus AlgorithmsOgnjen Maric, Christoph Sprenger, David Basin.
12:10 – 12:30 Towards Verifying Nonlinear Integer ArithmeticVincent Liew, Paul Beame.
12:30 – 14:00 Lunch
14:00 – 15:00 Networked and Distributed Systems. Chair: Bow-Yaw Wang
14:00 – 14:20 Network-wide Configuration SynthesisAhmed El-Hassany, Petar Tsankov, Laurent Vanbever, Martin Vechev.
14:20 – 14:40 Verifying Equivalence of Spark ProgramsShelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv.
14:40 – 15:00 Synchronization Synthesis for Network ProgramsJedidiah McClurg, Hossein Hojjat, Pavol Cerny.
15:00 – 15:30 Coffee break
15:30 – 16:40 Synthesis. Chair: Roopsha Samanta
15:30 – 15:40 BoSy: An experimentation framework for Bounded SynthesisPeter Faymonville, Bernd Finkbeiner, Leander Tentrup [Tool paper].
15:40 – 16:00 Bounded Synthesis for Streett, Rabin, and CTL*Ayrat Khalimov, Roderick Bloem.
16:00 – 16:20 Quantitative Assume Guarantee SynthesisShaull Almagor, Orna Kupferman, Jan Oliver Ringert, Yaron Velner.
16:20 – 16:40 Syntax-Guided Optimal Synthesis for Chemical Reaction NetworksLuca Cardelli, Milan Ceska, Martin Franzle, Marta Kwiatkowska, Luca Laurenti, Nicola Paoletti, Max Whitby.
17:00 – 18:00 Public Lecture. Chair: Roderick Bloem
17:00 – 18:00 Social Dynamics in the Post-Truth Society: How the Confirmation Bias is Changing the Public DiscourseFabiana Zollo.
18:30 Buses to castle start departing from Stadthalle
19:00 – evening Banquet
22:30 Buses going back from the castle start
Friday 28th July, Stadthalle
09:00 – 10:00 Invited Talk: Chair: Rupak MajumdarFormal reasoning under weak memory consistencyViktor Vafeiadis.
10:00 – 10:30 Coffee break
10:30 – 12:30 Decision Procedures and their Applications. Chair: Damien Zufferey
10:30 – 10:50 Model Counting for Recursively-Defined StringsMinh-Thai Trinh, Duc-Hiep Chu, Joxan Jaffar.
10:50 – 11:10 A Three-tier Strategy for Reasoning about Floating-Point Numbers in SMTSylvain Conchon, Mohamed Iguernlala, Kailiang Ji, Guillaume Melquiond, Clément Fumex.
11:10 – 11:30 A Correct-by-Decision Solution for Simultaneous Place and RouteAlexander Nadel.
11:30 – 11:50 Scaling Up DPLL(T) String Solvers using Context-Dependent SimplificationAndrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, Cesare Tinelli.
11:50 – 12:10 On Expansion and Resolution in CEGAR Based QBF SolvingLeander Tentrup.
12:10 – 12:30 A Decidable Fragment in Separation Logic with Inductive Predicates and ArithmeticQuang Loc Le, Tatsuta Makoto, Jun Sun, Wei-Ngan Chin.
12:30 – 14:00 Lunch
14:00 – 15:40 Software Analysis. Chair: Aws Albarghouthi
14:00 – 14:20 Finding Fix Locations for CFL-Reachability Analyses via Minimum CutsAndrei Marian Dan, Manu Sridharan, Satish Chandra, Jean-Baptiste Jeannin, Martin Vechev.
14:20 – 14:40 Proving linearizability using forward simulationsAhmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil.
14:40 – 14:50 EAHyper: Satisfiability, Implication, and Equivalence Checking of HyperpropertiesBernd Finkbeiner, Christopher Hahn, Marvin Stenger [Tool paper].
14:50 – 15:10 Automating Induction for Solving Horn ClausesHiroshi Unno, Sho Torii, Hiroki Sakamoto.
15:10 – 15:20 A Storm is Coming: A Modern Probabilistic Model CheckerChristian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk [Tool paper].
15:20 – 15:40 On Multiphase-Linear Ranking FunctionsAmir M. Ben-Amram, Samir Genaim.