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