Tuesday July 10
| 8:30 - 9:00: | Welcome | |
| 9:00 - 10:00: | “Synthesis and Some of Its Challenges” (Wolfgang Thomas - Keynote)
Chair: Madhusudan Parthasarathy | |
| 10:00 - 10:30: | Break |
| 10:30 - 12:00: | AUTOMATA AND SYNTHESIS - Chair: Roderick Bloem |
| R1 | Jan Kretinsky and Javier Esparza |
| Deterministic Automata for the (F,G)-fragment of LTL |
| R2 | Tomas Brazdil, Krishnendu Chatterjee, Antonin Kucera and Petr Novotny |
| Efficient Controller Synthesis for Consumption Games with Multiple Resource Types |
| R3 | Rüdiger Ehlers |
| ACTL ∩ LTL Synthesis |
| T1 | Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin and Jean-François Raskin |
| Acacia+, a tool for LTL synthesis |
| T2 | Chih-Hong Cheng, Michael Geisinger, Harald Ruess, Christian Buckl and Alois Knoll |
| MGSyn: Automatic Synthesis for Industrial Automation |
|
| 12:00 - 1:30: | Break |
| 1:30 - 3:35: | INDUCTIVE INFERENCE AND TERMINATION - Chair: Sriram Sankaranarayanan |
| R4 | Yu-Fang Chen and Bow-Yaw Wang |
| Learning Boolean Functions Incrementally |
| R5 | Rahul Sharma, Aditya Nori and Alex Aiken |
| Interpolants as Classifiers |
| R6 | Wonchan Lee, Bow-Yaw Wang and Kwangkeun Yi |
| Termination Analysis with Algorithmic Learning |
| R7 | Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl |
| Automated Termination Proofs for Java Programs with Cyclic Data |
| R8 | Javier Esparza, Andreas Gaiser and Stefan Kiefer |
| Proving Termination of Probabilistic Programs Using Patterns |
|
| 3:35 - 4:00: | Break |
| 4:00 - 6:05: | ABSTRACTION - Chair: Thomas Dillig |
| R9 | Arnaud Venet |
| The Gauge Domain: Scalable Analysis of Linear Inequality Invariants |
| R10 | Josh Berdine, Arlen Cox, Samin Ishtiaq and Christoph Wintersteiger |
| Diagnosing Abstraction Failure for Separation Logic-based Analyses |
| R11 | Aditya Thakur and Thomas Reps |
| A Method for Symbolic Computation of Abstract Operations |
| R12 | Simone Fulvio Rollini, Ondrej Sery and Natasha Sharygina |
| Leveraging Interpolant Strength in Model Checking |
| T3 | Evan Driscoll, Aditya Thakur and Thomas Reps |
| OpenNWA: A Nested Word Automaton Library |
| T4 | Aws Albarghouthi, Yi Li, Arie Gurfinkel and Marsha Chechik |
| UFO: A Framework for Abstraction- and Interpolation-Based Verification |
| T5 | Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina |
| SAFARI: SMT-based Abstraction For Arrays with Interpolants |
|
| 6:30 - 8:30: | PC dinner |
Wednesday July 11
| 8:35 - 10:35: | CONCURRENCY & SOFTWARE VERIFICATION - Chair: Zvonimir Rakamaric |
| R13 | Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi and Akash Lal |
| Detecting Fair Non-Termination in Multithreaded Programs |
| R14 | Vineet Kahlon and Chao Wang |
| Lock Removal for Concurrent Trace Programs |
| R15 | Gerhard Schellhorn, John Derrick and Heike Wehrheim |
| How to prove algorithms linearisable |
| R16 | Anthony Widjaja Lin and Matthew Hague |
| Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters |
| R17 | Alessandro Cimatti and Alberto Griggio |
| Software Model Checking via IC3 |
|
| 10:35 - 11:00: | Break |
| 11:00 - 12:00: | “Model Checking Cell Biology” (David Dill - Keynote)
Chair: Sanjit A. Seshia
|
| 12:00 - 1:30: | Lunch |
| 1:30 - 3:00: | BIOLOGY & PROBABILISTIC SYSTEMS - Chair: Mahesh Viswanathan |
| R18 | Calin Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu and Ali Sezgin |
| Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits |
| R19 | Anvesh Komuravelli, Corina S. Pasareanu and Edmund M. Clarke |
| Assume-Guarantee Abstraction Refinement for Probabilistic Systems |
| R20 | Cyrille Jegourel, Axel Legay and Sean Sedwards |
| Cross entropy optimisation of importance sampling parameters for statistical model checking |
| T6 | David Benque, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex Taylor and Moshe Vardi |
| Ripple: Visual Tool for Modeling and Analysis of Biological Networks |
| T7 | Stefan Kiefer, Andrzej Murawski, Joel Ouaknine, Björn Wachter and James Worrell |
| APEX: An analyzer for open probabilistic programs |
|
| 3:30 - 4:00: | Break |
| 4:00 - 5:30: | *EMBEDDED AND CONTROL SYSTEMS* - special track session - Chair: Stavros Tripakis |
| R21 | Adiya Zutshi, Sriram Sankaranarayanan and Ashish Tiwari |
| Timed Relational Abstractions For Sampled Data Control Systems |
| R22 | Rupak Majumdar and Majid Zamani |
| Approximately Bisimilar Symbolic Models for Digital Control Systems |
| R23 | Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya, Tiziana Rizzo, Marco Roveri, Angela Sanseviero and Andrei Tchaltsev |
| Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System
|
| T8 | Philip Armstrong, Joel Ouaknine, Hristina Palikareva and Bill Roscoe |
| Recent Developments in FDR |
| T9 | Songzheng Song, Jun Sun, Yang Liu and Jin Song Dong |
| A Model Checker for Hierarchical Probabilistic Real-time Systems |
|
| 6:00 - 9:30: | Banquet |
Thursday July 12
| 9:00 - 10:30: | *SAT/SMT SOLVING AND SMT-BASED VERIFICATION* - special track session - Chair: Orna Grumberg |
| R24 | Isil Dillig, Thomas Dillig, Kenneth McMillan and Alex Aiken |
| Minimum Satisfying Assignments for SMT |
| R25 | Cheng-Shen Han and Jie-Hong Roland Jiang |
| When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way |
| R26 | Akash Lal, Shaz Qadeer and Shuvendu Lahiri |
| A Solver for Reachability Modulo Theories |
| T10 | Shuvendu Lahiri, Chris Hawblitzel, Ming Kawaguchi and Henrique Rebêlo |
| SymDiff: A language-agnostic semantic diff tool |
| T11 | Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaidi |
| Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems |
|
| 10:30 - 11:00: | Break |
| 11:00 - 12:30: | TIMED & HYBRID SYSTEMS - Chair: Rajeev Alur |
| R27 | Shibashis Guha, Chinmay Narayan and S. Arun-Kumar |
| On Decidability of Prebisimulation for Timed Automata |
| R28 | Ichiro Hasuo and Kohei Suenaga |
| Exercises in Nonstandard Static Analysis of Hybrid Systems |
| R29 | Sergiy Bogomolov, Goran Frehse, Radu Grosu, Hamed Ladan, Andreas Podelski and Martin Wehrle |
| A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx |
| T12 | Ashish Tiwari |
| HybridSal Relational Abstracter |
| T13 | Swarat Chaudhuri and Armando Solar-Lezama |
| Euler: A System for Numerical Optimization of Programs |
|
| 12:30 - 2:00: | Lunch |
| 2:00 - 3:00: | *HARDWARE VERIFICATION* - special track session - Chair: William Hung |
| R30 | Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Scott Owens, Jade Alglave, Kayvan Memarian, Rajeev Alur, Milo Martin, Peter Sewell and Derek Williams |
| An Axiomatic Memory Model for Power Multiprocessors |
| R31 | Flavio M de Paula, Alan Hu and Amir Nahir |
| nuTAB-BackSpace: Rewriting to Normalize Non-Determinism in Post-Silicon Debug Traces |
| R32 | Zyad Hassan, Aaron Bradley and Fabio Somenzi |
| Incremental Inductive CTL Model Checking |
|
| 3:00 - 4:15: | Miscellaneous Tools - Chair: Aarti Gupta |
| T14 | Rishabh Singh and Armando Solar-Lezama |
| SPT : Storyboard Programming Tool |
| T15 | Patrick Rondon, Ming Kawaguchi, Alexander Bakst and Ranjit Jhala |
| CSolve: Verifying C With Liquid Types |
| T16 | Daniel Schwartz-Narbonne, Feng Liu, David August and Sharad Malik |
| PASSERT: A tool for debugging parallel programs |
| T17 | Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas and Andrew E. Santosa |
| TRACER: A Symbolic Execution Tool for Verification |
| T18 | Stephan Arlt and Martin Schäf |
| Joogie: Infeasible Code Detection for Java |
| T19 | David Hopkins, Andrzej Murawski and Luke Ong |
| Hector: An Equivalence Checker for a Higher-Order Fragment of ML |
| T20 | Jan Hoffmann, Klaus Aehlig and Martin Hofmann |
| Resource Aware ML |
|
| 4:15 - 6:00: | Tool demo/poster session |
| 6:00 - 7:00: | CAV business meeting |
| 7:00 - 9:00: | SC dinner |
Friday July 13
| 9:00 - 10:00: | Verifiably Insecure: Perils and Prospects of Electronic Voting (Alex Haldermann - Invited talk)
Chair: Somesh Jha
|
| 10:00 - 10:30: | Break |
| 10:30 - 11:45: | *SECURITY* - special track session - Chair: Swarat Chaudhuri |
| R33 | Matt Fredrikson, Richard Joiner, Somesh Jha, Thomas Reps, Phillip Porras, Hassen Saidi and Vinod Yegneswaran |
| Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement |
| R34 | Boris Köpf, Laurent Mauborgne and Martín Ochoa |
| Automatic Quantification of Cache Side-Channels |
| R35 | William Harris, Somesh Jha and Thomas Reps |
| Secure Programming via Visibly Pushdown Safety Games |
|
| 11:45 - 11:50: | Mini-break |
| 11:50 - 1:05: | VERIFICATION AND SYNTHESIS - Chair: Rupak Majumdar |
| R36 | Nishant Sinha, Nimit Singhania, Satish Chandra and Manu Sridharan |
| Alternate and Learn: Finding witnesses without looking all over |
| R37 | Duc Hiep Chu and Joxan Jaffar |
| A Complete Method for Symmetry Reduction in Safety Verification |
| R38 | Rishabh Singh and Sumit Gulwani |
| Synthesizing Number Transformations from Input-Output Examples |
|
| 1:00 - 1:15: | Conference Wrap-up |