Proceedings
The proceedings are available in two volumes: LNCS 9779 and LNCS 9780.
More information:
http://www.springer.com/978-
http://www.springer.com/978-
Online versions:
http://link.springer.com/ope
http://link.springer.com/ope
| July 19, 2016 [Tutorial Day] | ||
|---|---|---|
| 9:00am - 12:00pm | Parosh Abdulla Small Models in Parameterized Verification | Vitaly Chipounov The S2E Platform: Design, Implementation, and Applications |
| 12:00pm - 2:00pm | Lunch | |
| 2:00pm - 5:00pm | Paulo Tabuada Synthesizing Robust Cyber-Physical Systems | Martin Vechev and Pavol Bielik Machine Learning for Programs |
| 6:30pm | CAV Reception | |
| July 20, 2016 | |
|---|---|
| 8:45am - 9:00am | Welcome |
| 9:00am - 10:00am | Keynote Session chair: Azadeh Farzan Gilles Barthe (IMDEA) Computer-aided Cryptography |
| 10:00am - 10:30am | Break |
| 10:30am - 12:00pm | Probabilistic Systems Session chair: Roopsha Samanta Krishnendu Chatterjee, Hongfei Fu and Amir Kafshdar Goharshady. Termination Analysis of Probabilistic Programs through Positivstellensatz’s Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller and James Worrell. Markov Chains and Unambiguous Büchi Automata Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti and Justin Hsu. Synthesizing Probabilistic Invariants via Doob’s Decompositions Timon Gehr, Sasa Misailovic and Martin Vechev. PSI: Exact Symbolic Inference for Probabilistic Programs Van Chan Ngo, Axel Legay and Vania Joloboff. PSCV: A Runtime Verification Tool for Probabilistic SystemC Models [Short Talk] |
| 12:00pm - 2:00pm | Lunch |
| 2:00pm - 3:30pm | Synthesis I Session chair: Armando Solar-Lezama Chih-Hong Cheng, Yassine Hamsa and Harald Ruess Structural Synthesis for GXW Specifications Bernd Finkbeiner and Felix Klein Bounded Cycle Synthesis Tobias Klenze, Sam Bayless and Alan J. Hu Fast, Flexible, and Minimal CTL Synthesis via SMT Roderick Bloem, Nicolas Braud-Santoni and Swen Jacobs Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems Roderick Bloem and Swen Jacobs SYNTCOMP Results [Short Talk] Rishabh Singh SyGuS-COMP Results [Short Talk] |
| 3:30pm - 4:00pm | Break |
| 4:00pm - 5:30pm | Constraint-Solving I Session chair: Ruzica Piskac Maximiliano Cristia and Gianfranco Rossi A Decision Procedure for Sets, Binary Relations and Partial Functions Aina Niemetz, Mathias Preiner and Armin Biere Precise and Complete Propagation-based Local Search for Satisfiability Modulo Theories Minh-Thai Trinh, Duc-Hiep Chu and Joxan Jaffar Progressive Reasoning over Recursively-Defined Strings Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu and Jie-Hong R. Jiang String Analysis via Automata Manipulation with Logic Circuit Representation Bishoksan Kafle, John P. Gallagher and Jose F. Morales RAHFT: A Tool for Verifying Horn Clauses using Abstract Interpretation and Finite Tree Automata [Short Talk] |
| July 21, 2016 | |
|---|---|
| 8:45am - 10:00am | Presentation of CAV Award and Keynote Talk by an Award Winner Session chair: Ahmed Bouajjani |
| 10:00am - 10:30am | Break |
| 10:30am - 12:00pm | Model checking I Session chair: Aws Albarghouthi Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta and Sergio Mover Infinite-state Liveness-to-Safety via Implicit Abstraction and Well-founded Relations Michael Dooley and Fabio Somenzi Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances Fei He, Shu Mao and Bow-Yaw Wang Learning-based Assume-Guarantee Regression Verification Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu and Sharon Shoham Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement Temesghen Kahsai, Philipp Rümmer, Huascar Sanchez and Martin Schäf JayHorn: A Framework for Verifying Java programs [Short Talk] |
| 12:00pm - 2:00pm | Lunch |
| 2:00pm - 3:30pm | Program Analysis Session chair: Sharon Shoham K. Rustan M. Leino and Clément Pit–Claudel Trigger Selection Strategies to Stabilize Program Verifiers Quang Loc Le, Sun Jun and Wei-Ngan Chin Satisfiability Modulo Heap-Based Programs Peter Müller, Malte Schwerhoff and Alexander J. Summers Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution Roman Manevich, Boris Dogadov and Noam Rinetzky From Shape Analysis to Termination Analysis in Linear Time Dwight Guth, Chris Hathhorn, Manasvi Saxena, and Grigore Rosu RV-Match: Practical Semantics-Based Program Analysis [Short Talk] |
| 3:30pm - 4:00pm | Break |
| 4:00pm - 5:30pm | Timed and Hybrid Systems Session chair: Rajeev Alur Bai Xue, Zhikun She and Arvind Easwaran Under-Approximating Backward Reachable Sets by Polytopes Parasara Sridhar Duggirala and Mahesh Viswanathan Parsimonious Simulations Based Verification of Linear Systems Pavithra Prabhakar and Miriam García Soto Counterexample Guided Abstraction Refinement for Stability Analysis Bouyer Patricia, Colange Maximilien and Markey Nicolas Symbolic Optimal Reachability in Weighted Timed Automata Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan and Parasara Sridhar Duggirala Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2 [Short] |
| 5:30pm - 7:00pm | CAV Business Meeting |
| July 22, 2016 | |
|---|---|
| 9:00am - 10:00am | Keynote Session chair: Clark Barrett Gerwin Klein (NICTA and University of New South Wales) Scaling Up - From Trustworthy seL4 to Trustworthy Systems |
| 10:00am - 10:30am | Break |
| 10:30am - 12:00pm | Verification in Practice Session chair: Bow-Yaw Wang Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta and Kristin Yvonne Rozier Model Checking at Scale: Automated Air Traffic Control Design Space Exploration Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst and Jonathan Jacky Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel and Ali Zaidi End-to-End Verification of ARM Processors with ISA-Formal FengWei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li A Practical Verification Framework for Preemptive OS Kernels Mark Santolucito, Ennan Zhai and Ruzica Piskac Probabilistic Automated Language Learning for Configuration Files |
| 12:00pm - 2:00pm | Lunch |
| 2:00pm - 3:30pm | Concurrency Session chair: Pavol Cerny Yu-Fang Chen, Song Lei and Zhilin Wu The Commutativity Problem of the MapReduce Framework: A Transducer-based Approach Anthony W. Lin and Philipp Ruemmer Liveness of Randomised Parameterised Systems under Arbitrary Schedulers Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson and Carl Leonardsson Stateless Model Checking for POWER Dmitry Chistikov, Rupak Majumdar and Filip Niksic Hitting Families of Schedules for Asynchronous Programs Vladimir Herdt, Hoang M. Le, Daniel Große and Rolf Drechsler ParCoSS: Efficient Parallelized Compiled Symbolic Simulation [Short] |
| 3:30pm - 4:00pm | Break |
| 4:00pm - 5:00pm | Constraint-Solving II Session chair: Thomas Wies Zhoulai Fu and Zhendong Su XSat: A Fast Floating-Point Satisfiability Solver Samuel Drews and Aws Albarghouthi. Effectively Propositional Interpolants Przemyslaw Daca, Thomas A. Henzinger and Andrey Kupriyanov Array Folds Logic |
| 5:30pm - 6:30pm | Logic Lounge with Moshe Vardi in memoriam Helmut Veith Venue: University of Toronto Bahen Building - Room 1160 (short name BA1160) 40 St. George Street Toronto, ON, Canada M5S 2E4 |
| 7:00pm - 10:00pm | CAV Banquet at Art Gallery of Ontario (directions). Note: The banquet venue will be open for attendees from 6:45pm. Also, the gallery will be open late for visitors. |
| July 23, 2016 | |
|---|---|
| 9:00am - 10:00am | Keynote Session chair: Swarat Chaudhuri Moshe Vardi (Rice University) Constrained Sampling and Counting |
| 10:00am - 10:30am | Break |
| 10:30am - 12:00pm | Automata and Games Session chair: Fabio Somenzi Rajeev Alur, Salar Moarref and Ufuk Topcu Compositional Synthesis of Reactive Controllers for Multi-Agent Systems Massimo Benerecetti, Daniele Dell’Erba and Fabio Mogavero Solving Parity Games via Priority Promotion Ernst Moritz Hahn, Sven Schewe, Andrea Turrini and Lijun Zhang A Simple Algorithm for Solving Qualitative Probabilistic Parity Games Salomon Sickert, Javier Esparza, Stefan Jaax and Jan Křetínský Limit-Deterministic Büchi Automata for Linear Temporal Logic Ruediger Ehlers and Vasumathi Raman Slugs: Extensible GR(1) Synthesis [Short] |
| 12:00pm - 2:00pm | Lunch |
| 2:00pm - 3:30pm | Synthesis II Session chair: Roderick Bloem Hassan Eldib, Meng Wu and Chao Wang Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits Alexander Legg, Nina Narodytska and Leonid Ryzhyk A SAT-Based Counterexample Guided Method for Unbounded Synthesis Loris D’Antoni, Roopsha Samanta and Rishabh Singh Qlose: Program Repair with Quantitative Objectives Dror Fried, Lucas M. Tabajara and Moshe Y. Vardi BDD-Based Boolean Functional Synthesis Bernhard Scholz, Herbert Jordan and Pavle Subotic. Souffle: On Synthesis of Datalog for Program Analyzers [Short] |
| 3:30pm - 4:00pm | Break |
| 4:00pm - 5:30pm | Model Checking II Session chair: Constantin Enea Grigory Fedyukovich, Arie Gurfinkel and Natasha Sharygina Property Directed Equivalence via Abstract Simulation Paul Fiterau-Brostean, Ramon Janssen and Frits Vaandrager Combining Model Checking and Automata Learning to Analyze TCP Implementations Anton Wijs BFS-Based Model Checking of Linear-Time Properties With An Application on GPUs Michele Sevegnani, Muffy Calder and Michele Sevegnani BigraphER: rewriting and analysis engine for bigraphs [Short] Dirk Beyer and Matthias Dangl Verification-Aided Debugging: A Convenient Web-Service for Witness Exploration [Short] Adrien Champion, Alain Mebsout, Christoph Sticksel and Cesare Tinelli The KIND 2 Model-Checker [Short] |
| 5:30pm - 5:45pm | Closing |