Accepted Papers

Philipp Ruemmer, Hossein Hojjat and Viktor Kuncak       Disjunctive Interpolants for Horn-Clause Verification
Oshri Adler, Cindy Eisner and Tatyana Veksler   Relative Equivalence in the Presence of Ambiguity
Alberto Puggelli, Wenchao Li, Alberto Sangiovanni-Vincentelli and Sanjit Seshia   Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties
Hui Kong, Fei He, Xiaoyu Song, William Hung and Ming Gu   Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems
Guanfeng Lv, Kaile Su and Yanyan Xu   CacBDD: A BDD Package with Dynamic Cache Management
Andrew Reynolds, Cesare Tinelli, Amit Goel and Sava Krstic   Finite Model Finding in SMT
Pierre Ganty and Samir Genaim   Proving Termination Starting from the End
Supratik Chakraborty, Kuldeep S. Meel and Moshe Vardi   A Scalable and Nearly Uniform Generator of SAT Witnesses
Marc Brockschmidt, Byron Cook and Carsten Fuhs   Better termination proving through cooperation
Chih-Hong Cheng, Harald Ruess and Natarajan Shankar   JBernstein: A Validity Checker for Generalized Polynomial Constraints
Arun Chaganty, Akash Lal, Aditya Nori and Sriram Rajamani   Combining Relational Learning with SMT Solvers using CEGAR
Krishnendu Chatterjee and Jakub Łącki   Faster Algorithms for Markov Decision Processes with Low Treewidth
Christoph Haase, Samin Ishtiaq, Joel Ouaknine and Matthew Parkinson   SeLoger: A Tool for Graph-Based Reasoning in Separation Logic
William Harris, Guoliang Jin, Shan Lu and Somesh Jha   Validating Library Usage Interactively
Isil Dillig and Thomas Dillig   EXPLAIN: A Tool for Performing Abductive Inference
Brad Bingham, Jesse Bingham, John Erickson and Mark Greenstreet   Distributed Explicit State Model Checking of Deadlock Freedom
Pranav Garg, Christof Loding, P. Madhusudan and Daniel Neider   Learning Universally Quantified Invariants of Linear Data Structures
Cezara Dragoi, Ashutosh Gupta and Thomas Henzinger   Automatic linearizability proofs of concurrent objects with cooperating updates
Aleksandar Chakarov and Sriram Sankaranarayanan   Probabilistic Program Analysis with Martingales
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, Fabio Merli and Enrico Tronci   System Level Formal Verification via Model Checking Driven Simulation
Romain Brenguier   PRALINE: A Tool for Computing Nash Equilibria in Concurrent   Games
Simon Meier, Benedikt Schmidt, Cas Cremers and David Basin   The TAMARIN Prover for the Symbolic Analysis of Security Protocols
Johannes G. Reiter, Ivana Bozic, Krishnendu Chatterjee and Martin A. Nowak   TTP: Tool for Tumor Progression
Adi Sosnovich, Orna Grumberg and Gabi Nakibly   Finding Security Vulnerabilities in a Network Protocol using Parameterized Systems
Krishnendu Chatterjee, Andreas Gaiser and Jan Kretinsky   Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki and Edmund Clarke   Automatic Abstraction in SMT-Based Unbounded Software Model Checking
Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach   Efficient synthesis for concurrency using semantics-preserving transformations
Jade Alglave, Daniel Kroening and Michael Tautschnig   Partial Orders for Efficient BMC of Concurrent Software
Azadeh Farzan and Zachary Kincaid   Duet: Static Analysis for Unbounded Parallelism
Roy Armoni, Dana Fisman and Naiyong Jin   SVA and PSL Local Variables – A Practical Approach
Aws Albarghouthi and Ken Mcmillan   Beautiful Interpolants
Ocan Sankur   Shrinktech: A Tool for the Robustness Analysis of Timed Automata
Jiri Barnat, Lubos Brim, Vojtěch Havel, Jan Havlíček, Jan Kriho, Milan Lenco, Petr Ročkai, Vladimír Štill and Jiří Weiser   DiVinE 3.0 — Explicit-state Model-checker for Multithreaded C/C++  Programs
Tom Chothia, Yusuke Kawamoto and Chris Novakovic   A Tool for Estimating Information Leakage
Koen Claessen, Jasmin Fisher, Samin Ishtiaq, Nir Piterman and Qinsi Wang   Model-Checking Signal Transduction Networks through Decreasing Reachability Sets
Shaull Almagor, Guy Avni and Orna Kupferman   Automatic Generation of Quality Specifications
Loris D’Antoni and Margus Veanes   Equivalence of Extended Symbolic Finite Transducers
Pierre Ganty, Javier Esparza and Rupak Majumdar   Parameterized Verification of Asynchronous Shared-Memory Systems
Thomas Braibant and Adam Chlipala   Formal Verification of Hardware Synthesis
Vincent Cheval, Veronique Cortier and Antoine Plet   Lengths may break privacy — or how to check for equivalences with length
Fabrizio Biondi, Andrzej Wasowski, Axel Legay and Louis-Marie Traonouez   QUAIL: a quantitative security analyzer for imperative code
Ruzica Piskac, Thomas Wies and Damien Zufferey   Automating Separation Logic using SMT
Pavithra Prabhakar and Miriam Garcia Soto   Abstraction based Model-Checking of Stability of Hybrid Systems
Alfons Laarman, Mads Chr. Olesen, Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen and Jaco Van De Pol   Multi-Core Emptiness Checking of Timed B\”uchi Automata using Inclusion Abstraction
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleks Nanevski and Mooly Sagiv   Effectively Propositional Reasoning about Reachability in Linked Data Structures
Lubos Brim, Milan Ceska, Sven Drazan and David Šafránek   Exploring Parameter Space of Stochastic Biochemical Systems using  Quantitative Model Checking
Daniel Wonisch, Alexander Schremmer and Heike Wehrheim   Programs from Proofs – A PCC Alternative
Richard Uhler and Nirav Dave   Seri: Automatic Translation of High-level Symbolic Computations into SMT Queries
Maximilien Colange, Souheib Baarir, Fabrice Kordon and Yann Thierry-Mieg   Towards Software Model Checking using Data Decision Diagrams
Cyrille Jegourel, Axel Legay and Sean Sedwards   Importance Splitting for Statistical Model Checking Rare Properties
Aws Albarghouthi, Sumit Gulwani and Zachary Kincaid   Recursive Program Synthesis
Daniel Kroening, Matt Lewis and Georg Weissenbacher   Under-Approximating Loops in C Programs for Fast Counterexample Detection
Alexandre Donzé, Thomas Ferrere and Oded Maler   Efficient Robust Monitoring for STL
Tewodros Beyene, Corneliu Popeea and Andrey Rybalchenko   Solving Existentially Quantified Horn Clauses
Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf and Jan-Georg Smaus   A Fully Verified Executable LTL Model Checker
Christian Von Essen and Barbara Jobstmann   Program Repair without Regret
Alistair Stewart, Kousha Etessami and Mihalis Yannakakis   Upper bounds for Newton’s method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata
Sudhindra Pandav, Maheshwar Singh and Hemanthkumar Sivaraj   End-to-end Runtime Validation of Intel(R) Transactional Synchronization Extensions
Yakir Vizel, Vadim Ryvchin and Alexander Nadel   Efficient Generation of Small Interpolants in CNF
Frédéric Herbreteau, B Srivathsan and Igor Walukiewicz   Lazy abstractions for timed automata
Xin Chen, Erika Abraham and Sriram Sankaranarayanan   Flow*: An Analyzer for Non-Linear Hybrid Systems
Loïc Paulevé, Geoffroy Andrieux and Heinz Koeppl   Under-approximating Cut Sets for Reachability in Large Scale Automata Networks
Joao Marques-Silva, Mikolas Janota and Anton Belov   Minimal Sets over Monotone Predicates in Boolean Formulae
Johannes Kloos, Rupak Majumdar, Filip Niksic and Ruzica Piskac   Incremental, Inductive Coverability
Étienne André, Yang Liu, Jun Sun, Jin Song Dong and Shang-Wei Lin   PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems
Panagiotis Manolios and Vasilis Papavasileiou   ILP Modulo Theories
Liyun Dai, Bican Xia and Naijun Zhan   Generating Non-Linear Interpolants by Semidefinite Programming
Ming-Hsien Tsai, Yih-Kuen Tsay and Yu-Shiang Hwang   GOAL for Games, Omega-Automata, and Logics
Lukas Holik, Ondrej Lengal, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar   Fully Automated Shape Analysis Based on Forest Automata
Ayrat Khalimov, Swen Jacobs and Roderick Bloem   PARTY: Parameterized Synthesis of Token Rings