Invited Contribution |
Quantitative Models for a Not So Dumb Grid / Holger Hermanns |
SAT and SMT Based Methods |
History-Aware Data Structure Repair Using SAT / Razieh Nokhbeh Zaeem ; Divya Gopinath ; Sarfraz Khurshid ; Kathryn S. McKinley |
The Guardol Language and Verification System / David Hardin ; Konrad Slind ; Michael Whalen ; Tuan-Hung Pham |
A Bit Too Precise? Bounded Verification of Quantized Digital Filters / Arlen Cox ; Sriram Sankaranarayanan ; Bor-Yuh Evan Chang |
Numeric Bounds Analysis with Conflict-Driven Learning / Vijay D'Silva ; Leopold Haller ; Daniel Kroening ; Michael Tautschnig |
Automata |
Ramsey-Based Analysis of Parity Automata / Oliver Friedmann ; Martin Lange |
VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata / Ondrej Lengál ; Jirí Simácek ; Tomáš Vojnar |
LTL to Büchi Automata Translation: Fast and More Deterministic / Tomáš Babiak ; Mojmír Kretínský ; Vojtech Rehák ; Jan Strejcek |
Model Checking |
Pushdown Model Checking for Malware Detection / Fu Song ; Tayssir Touili |
Aspect-Oriented Runtime Monitor Certification / Kevin W. Hamlen ; Micah M. Jones ; Meera Sridhar |
Partial Model Checking Using Networks of Labelled Transition Systems and Boolean Equation Systems / Frédéric Lang ; Radu Mateescu |
From Under-Approximations to Over-Approximations and Back / Aws Albarghouthi ; Arie Gurfinkel ; Marsha Chechik |
Case Studies |
Automated Analysis of AODV Using UPPAAL / Ansgar Fehnker ; Rob van Glabbeek ; Peter Höfner ; Annabelle McIver ; Marius Portmann ; Wee Lum Tan |
Modeling and Verification of a Dual Chamber Implantable Pacemaker / Zhihao Jiang ; Miroslav Pajic ; Salar Moarref ; Rajeev Alur ; Rahul Mangharam |
Memory Models and Termination |
Counter-Example Guided Fence Insertion under TSO / Parosh Aziz Abdulla ; Mohamed Faouzi Atig ; Yu-Fang Chen ; Carl Leonardsson ; Ahmed Rezine |
Java Memory Model-Aware Model Checking / Huafeng Jin ; Tuba Yavuz-Kahveci ; Beverly A. Sanders |
Compositional Termination Proofs for Multi-threaded Programs / Corneliu Popeea ; Andrey Rybalchenko |
Deciding Conditional Termination / Marius Bozga ; Radu Iosif ; Filip Konecný |
Internet Protocol Verification |
The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures / Alessandro Armando ; Wihem Arsac ; Tigran Avanesov ; Michele Barletta ; Alberto Calvi ; Alessandro Cappai ; Roberto Carbone ; Yannick Chevalier ; Luca Compagna ; Jorge Cuéllar ; Gabriel Erzse ; Simone Frau ; Marius Minea ; Sebastian Mödersheim ; David von Oheimb ; Giancarlo Pellegrino ; Serena Elisa Ponta ; Marco Rocchetto ; Michael Rusinowitch ; Mohammad Torabi Dashti ; Mathieu Turuani ; Luca Viganò |
Reduction-Based Formal Analysis of BGP Instances / Anduo Wang ; Carolyn Talcott ; Alexander J.T. Gurney ; Boon Thau Loo ; Andre Scedrov |
Stochastic Model Checking |
Minimal Critical Subsystems for Discrete-Time Markov Models / Ralf Wimmer ; Nils Jansen ; Erika Ábrahám ; Bernd Becker ; Joost-Pieter Katoen |
Automatic Verification of Competitive Stochastic Systems / Taolue Chen ; Vojtech Forejt ; Marta Kwiatkowska ; David Parker ; Aistis Simaitis |
Coupling and Importance Sampling for Statistical Model Checking / Benoit Barbot ; Serge Haddad ; Claudine Picaronny |
Verifying pCTL Model Checking / Johannes Hölzl ; Tobias Nipkow |
Synthesis |
Parameterized Synthesis / Swen Jacobs ; Roderick Bloem |
QuteRTL: Towards an Open Source Framework for RTL Design Synthesis and Verification / Hu-Hsi Yeh ; Cheng-Yin Wu ; Chung-Yang (Ric) Huang |
Template-Based Controller Synthesis for Timed Systems / Bernd Finkbeiner ; Hans-Jörg Peter |
Provers and Analysis Techniques |
Zeno: An Automated Prover for Properties of Recursive Data Structures / William Sonnex ; Sophia Drossopoulou ; Susan Eisenbach |
A Proof Assistant for Alloy Specifications / Mattias Ulbrich ; Ulrich Geilmann ; Aboubakr Achraf El Ghazi ; Mana Taghdiri |
Reachability under Contextual Locking / Rohit Chadha ; P. Madhusudan ; Mahesh Viswanathan |
Bounded Phase Analysis of Message-Passing Programs / Ahmed Bouajjani ; Michael Emmi |
Tool Demonstrations |
Demonstrating Learning of Register Automata / Maik Merten ; Falk Howar ; Bernhard Steffen ; Sofia Cassel ; Bengt Jonsson |
Symbolic Automata: The Toolkit / Margus Veanes ; Nikolaj Bjørner |
McScM: A General Framework for the Verification of Communicating Machines / Alexander Heuβner ; Tristan Le Gall ; Grégoire Sutre |
SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications / Luís Caires ; Hugo Torres Vieira |
TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets / Alexandre David ; Lasse Jacobsen ; Morten Jacobsen ; Kenneth Yrke Jørgensen ; Mikael H. Møller ; Jirí Srba |
A Platform for High Performance Statistical Model Checking - PLASMA / Cyrille Jegourel ; Axel Legay ; Sean Sedwards |
Competition on Software Verification |
Competition on Software Verification (SV-COMP) / Dirk Beyer |
Predicate Analysis with BLAST 2.7 (Competition Contribution) / Pavel Shved ; Mikhail Mandrykin ; Vadim Mutilin |
CPAchecker with Adjustable Predicate Analysis (Competition Contribution) / Stefan Löwe ; Philipp Wendler |
Block Abstraction Memoization for CPAchecker (Competition Contribution) / Daniel Wonisch |
Context-Bounded Model Checking with ESBMC 1.17 (Competition Contribution) / Lucas Cordeiro ; Jeremy Morse ; Denis Nicole ; Bernd Fischer |
Proving Reachability Using FShell (Competition Contribution) / Andreas Holzer ; Christian Schallhart ; Helmut Veith |
LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation (Competition Contribution) / Carsten Sinz ; Florian Merz ; Stephan Falke |
Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution) / Kamil Dudka ; Petr Müller ; Petr Peringer |
HSF(C): A Software Verifier Based on Horn Clauses (Competition Contribution) / Sergey Grebenshchikov ; Ashutosh Gupta ; Nuno P. Lopes |
SatAbs: A Bit-Precise Verifier for C Programs (Competition Contribution) / Gérard Basler ; Alastair Donaldson ; Alexander Kaiser ; Thomas Wahl |
Wolverine: Battling Bugs with Interpolants (Competition Contribution) / Georg Weissenbacher ; Sharad Malik |
Author Index |
Invited Contribution |
Quantitative Models for a Not So Dumb Grid / Holger Hermanns |
SAT and SMT Based Methods |