Accepted Papers

Regular Papers

  1. Krishnendu Chatterjee, Hongfei Fu and Amir Kafshdar Goharshady. Termination Analysis of Probabilistic Programs through Positivstellensatz’s
  2. Hassan Eldib, Meng Wu and Chao Wang. Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits
  3. Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta and Kristin Yvonne Rozier. Model Checking at Scale: Automated Air Traffic Control Design Space Exploration
  4. 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
  5. Yu-Fang Chen, Song Lei and Zhilin Wu. The Commutativity Problem of the MapReduce Framework: A Transducer-based Approach
  6. Chih-Hong Cheng, Yassine Hamsa and Harald Ruess. Structural Synthesis for GXW Specifications
  7. Paul Fiterau-Brostean, Ramon Janssen, Frits Vaandrager and Paul Fiterau Brostean. Combining Model Checking and Automata Learning to Analyze TCP Implementations
  8. Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta and Sergio Mover. Infinite-state Liveness-to-Safety via Implicit Abstraction and Well-founded Relations
  9. Christel Baier, Stefan Kiefer, Joachim Klein, Sascha Klüppelholz, David Müller and James Worrell. Markov Chains and Unambiguous Büchi Automata
  10. Salomon Sickert, Javier Esparza, Stefan Jaax and Jan Křetínský. Limit-Deterministic Büchi Automata for Linear Temporal Logic
  11. Fei He, Shu Mao and Bow-Yaw Wang. Learning-based Assume-Guarantee Regression Verification
  12. 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
  13. Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu and Sharon Shoham. Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement
  14. Samuel Drews and Aws Albarghouthi. Effectively Propositional Interpolants
  15. Loris D’Antoni, Roopsha Samanta and Rishabh Singh. Qlose: Program Repair with Quantitative Objectives
  16. FengWei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, Zhaohui Li and Ming Fu. A Practical Verification Framework for Preemptive OS Kernels
  17. Massimo Benerecetti, Daniele Dell’Erba and Fabio Mogavero. Solving Parity Games via Priority Promotion
  18. Bouyer Patricia, Colange Maximilien and Markey Nicolas. Symbolic Optimal Reachability in Weighted Timed Automata
  19. Bai Xue, Zhikun She, Arvind Easwaran and Bai Xue. Under-Approximating Backward Reachable Sets by Polytopes
  20. Maximiliano Cristia and Gianfranco Rossi. A Decision Procedure for Sets, Binary Relations and Partial Functions
  21. Aina Niemetz, Mathias Preiner and Armin Biere. Precise and Complete Propagation-based Local Search for Satisfiability Modulo Theories
  22. K. Rustan M. Leino and Clément Pit–Claudel. Trigger selection strategies to stabilize program verifiers
  23. Dror Fried, Lucas M. Tabajara and Moshe Y. Vardi. BDD-Based Boolean Functional Synthesis
  24. Rajeev Alur, Salar Moarref and Ufuk Topcu. Compositional Synthesis of Reactive Controllers for Multi-Agent Systems
  25. Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti and Justin Hsu. Synthesizing Probabilistic Invariants via Doob’s Decompositions
  26. Alexander Legg, Nina Narodytska and Leonid Ryzhyk. A SAT-Based Counterexample Guided Method for Unbounded Synthesis
  27. Ernst Moritz Hahn, Sven Schewe, Andrea Turrini and Lijun Zhang.A Simple Algorithm for Solving Qualitative Probabilistic Parity Games
  28. Anthony W. Lin and Philipp Ruemmer. Liveness of Randomised Parameterised Systems under Arbitrary Schedulers
  29. Parasara Sridhar Duggirala and Mahesh Viswanathan. Parsimonious Simulations Based Verification of Linear Systems
  30. Minh-Thai Trinh, Duc-Hiep Chu and Joxan Jaffar. Progressive Reasoning over Recursively-Defined Strings
  31. Timon Gehr, Sasa Misailovic and Martin Vechev. PSI: Exact Symbolic Inference for Probabilistic Programs
  32. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson and Carl Leonardsson. Stateless Model Checking for POWER
  33. Quang Loc Le, Sun Jun and Wei-Ngan Chin. Satisfiability Modulo Heap-Based Programs
  34. 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
  35. Peter Müller, Malte Schwerhoff and Alexander J. Summers. Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution
  36. Pavithra Prabhakar and Miriam García Soto. Counterexample Guided Abstraction Refinement for Stability Analysis
  37. Bernd Finkbeiner and Felix Klein. Bounded Cycle Synthesis
  38. Grigory Fedyukovich, Arie Gurfinkel and Natasha Sharygina. Property Directed Equivalence via Abstract Simulation
  39. Zhoulai Fu and Zhendong Su. XSat: A Fast Floating-Point Satisfiability Solver
  40. Tobias Klenze, Sam Bayless and Alan J. Hu. Fast, Flexible, and Minimal CTL Synthesis via SMT
  41. Roderick Bloem, Nicolas Braud-Santoni and Swen Jacobs. Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems
  42. Dmitry Chistikov, Rupak Majumdar and Filip Niksic. Hitting Families of Schedules for Asynchronous Programs
  43. Michael Dooley and Fabio Somenzi. Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances
  44. Przemyslaw Daca, Thomas A. Henzinger and Andrey Kupriyanov. Array Folds Logic
  45. Anton Wijs. BFS-Based Model Checking of Linear-Time Properties With An Application on GPUs
  46. Roman Manevich, Boris Dogadov and Noam Rinetzky. From Shape Analysis to Termination Analysis in Linear Time

Tool Papers

  1. Vladimir Herdt, Hoang M. Le, Daniel Große and Rolf Drechsler. ParCoSS: Efficient Parallelized Compiled Symbolic Simulation
  2. Michele Sevegnani, Muffy Calder and Michele Sevegnani. BigraphER: rewriting and analysis engine for bigraphs
  3. Adrien Champion, Alain Mebsout, Christoph Sticksel and Cesare Tinelli. The KIND 2 Model-Checker
  4. Temesghen Kahsai, Philipp Rümmer, Huascar Sanchez and Martin Schäf. JayHorn: A Framework for Verifying Java programs
  5. Mark Santolucito, Ennan Zhai and Ruzica Piskac. Probabilistic Automated Language Learning for Configuration Files
  6. Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan and Parasara Sridhar Duggirala. Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2
  7. Ruediger Ehlers and Vasumathi Raman. Slugs: Extensible GR(1) Synthesis
  8. Van Chan Ngo, Axel Legay and Vania Joloboff. PSCV: A Runtime Verification Tool for Probabilistic SystemC Models
  9. Bishoksan Kafle, John P. Gallagher and Jose F. Morales. RAHFT: A Tool for Verifying Horn Clauses using Abstract Interpretation and Finite Tree Automata
  10. Dirk Beyer and Matthias Dangl. Verification-Aided Debugging: A Convenient Web-Service for Witness Exploration
  11. Dwight Guth, Chris Hathhorn, Manasvi Saxena, and Grigore Rosu. RV-Match: Practical Semantics-Based Program Analysis
  12. Bernhard Scholz, Herbert Jordan and Pavle Subotic. Souffle: On Synthesis of Datalog for Program Analyzers