Accepted Papers

Regular Papers

Ashutosh Gupta. Improved Single Pass Algorithms for Resolution Proof Reduction
Krishnendu Chatterjee, Martin Chmelík and Rupak Majumdar. Equivalence of Games with Probabilistic Uncertainty and Partial-observation Games
Mohamed Amin Ben Sassi, Romain Testylier, Thao Dang and Antoine Girard. Reachability Analysis of Polynomial Systems using Linear Programming Relaxations.
Matthias Guedemann, Gwen Salaün and Meriem Ouederni. Counterexample Guided Synthesis of Monitors for Realizability Enforcement
Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate. Higher-Order Approximations for Verification of Stochastic Hybrid Systems
Hossein Hojjat, Radu Iosif, Filip Konecny, Viktor Kuncak and Philipp Ruemmer. Accelerating Interpolants
Simoni Shah and Paritosh Pandya. The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints
Luis María Ferrer Fioriti, Ernst Moritz Hahn, Holger Hermanns and Björn Wachter. Variable Probabilistic Abstraction Refinement
Sarai Sheinvald, Orna Grumberg and Orna Kupferman. Model Checking Systems and Specifications with Parameterized Atomic Propositions
Shulamit Halamish and Orna Kupferman. Approximating Deterministic Lattice Automata
Daniel Neider. Computing Minimal Separating DFAs and Regular Invariants Using SAT and SMT Solvers
Benedikt Bollig, Paul Gastin, Benjamin Monmege and Marc Zeitoun. A Probabilistic Kleene Theorem
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea and Mihaela Sighireanu. Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data
John Fearnley, Doron Peled and Sven Schewe. Synthesis of Succinct Systems
Alexandre Donzé, Oded Maler, Ezio Bartocci, Dejan Nickovic, Radu Grosu and Scott Smolka. On Temporal Logic and Signal Processing
Rodrigo T. Saad, Silvano Dal Zilio and Bernard Berthomieu. An Experiment on Parallel Model Checking of a CTL Fragment
Sofia Cassel, Bengt Jonsson, Falk Howar and Bernhard Steffen. A Succinct Canonical Register Automaton Model for Data Domains with Binary Relations
Sami Evangelista, Alfons Laarman, Laure Petrucci and Jaco Van De Pol. Improved Multi-Core Nested Depth-First Search
Peter Bulychev, Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Jean-Francois Raskin and Pierre-Alain Reynier. Controllers with Minimal Observation Power (Application to Timed Systems)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar and Prakash Saivasan. Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding
Vojtech Forejt, Marta Kwiatkowska and David Parker. Pareto Curves for Probabilistic Model Checking
Bernd Becker, Rüdiger Ehlers, Matthew Lewis and Paolo Marin. ALLQBF Solving by Computational Learning
Sergio Giro and Markus N. Rabe. Verification of partial-information probabilistic systems using counterexample-guided refinements
Sven Schewe and Thomas Varghese. Tight Bounds for the Determinisation and Complementation of Generalised Buchi Automata
Daniel Schwartz-Narbonne, Georg Weissenbacher and Sharad Malik. Parallel Assertions for Architectures with Weak Memory Models

Tool Papers

Ondrej Sery, Grigory Fedyukovich and Natasha Sharygina. FunFrog: Bounded Model Checking with Interpolation-based Function Summarization
Nils Jansen, Erika Abraham, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen and Bernd Becker. The COMICS Tool – Computing Minimal Counterexamples for DTMCs
Andreas Gaiser, Jan Kretinsky and Javier Esparza. Rabinizer: Small Deterministic Automata for LTL(F,G)
Carlo Alberto Furia. A Verifier for Functional Properties of Sequence-Manipulating Programs