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 |