Accepted Papers


Out of 108 submitted papers, 33 were accepted, including 24 regular papers and 9 short papers.

Regular papers

Martín Abadi and Michael Isard
Timely Rollback: Specification and Verification

Aboubakr Achraf El Ghazi, Mana Taghdiri and Mihai Herda
First-Order Transitive Closure Axiomatization via Iterative Invariant Injections

Gianluca Amato, Simone Di Nardo Di Maio and Francesca Scozzari
Sum of Abstract Domains

Étienne André, Giuseppe Lipari, Hoang Gia Nguyen and Youcheng Sun
Reachability Preservation Based Parameter Synthesis for Timed Automata

Lacramioara Astefanoaei, Ben Rayana Souha, Saddek Bensalem, Marius Bozga and Jacques Combaz
Compositional Verification of Parameterised Timed Systems

John Backes, Darren Cofer, Steven Miller and Michael Whalen
Requirements Analysis of a Quad-Redundant Flight Control System

Dragan Bosnacki and Mark Scheffer
Partial Order Reduction and Symmetry with Multiple Representatives

Alice Dal Corso, Damiano Macedonio and Massimo Merro
Statistical Model Checking of Ad Hoc Routing Protocols in Lossy Grid Networks

Tommaso Dreossi, Thao Dang, Alexandre Donzé, James Kapinski, Jyotirmoy Deshmukh and Xiaoqing Jin
Efficient Guiding Strategies for Testing of Temporal Properties of Hybrid Systems

Andrew Fisher, Chris Myers and Peng Li
Reachability Analysis Using Extremal Rates

Andrew Gacek, Andreas Katis, Michael Whalen, John Backes and Darren Cofer
Towards Realizability Checking of Contracts using Theories

Thomas Gibson-Robinson, Henri Hansen, Bill Roscoe and Xu Wang
Practical Partial Order Reduction for CSP

Alex Groce and Jervis Pinto
A Little Language for Testing

Yu Huang and Eric Mercer
Detecting MPI Zero Buffer Incompatibility by SMT Encoding

Robert Jakob and Peter Thiemann
A Falsification View of Success Typing

Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich and Insup Lee
Verified ROS-Based Deployment of Platform-Independent Control Systems

Rajiv Murali, Andrew Ireland and Gudmund Grov
A Rigorous Approach to Combining Use Case Modelling and Accident Scenarios

Anitha Murugesan, Michael Whalen, Neha Rungta, Oksana Tkachuk, Suzette Person, Mats Heimdahl and Dongjiang You
Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites

Yan Peng and Mark Greenstreet
Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification

Shashank Pathak, Erika Abraham, Nils Jansen, Armando Tacchella and Joost-Pieter Katoen
A Greedy Approach for the Efficient Repair of Stochastic Models

Holger Siegel and Axel Simon
Shape Analysis with Connectors

Daniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanović, Philipp Rümmer and Thomas Wies
Conflict-Directed Graph Coverage

Freek Verbeek, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum, Oto Havle, Bruno Langenstein, Werner Stephan and Burkhart Wolff
Formal Functional Specification of the PikeOS Separation Kernel

Ahlem Triki, Borzoo Bonakdarpour, Jacques Combaz and Saddek Bensalem
Automated Conflict-Free Concurrent Implementation of Timed Component-Based Models

Short papers

Ivan Bocic and Tevfik Bultan
Data Model Bugs

Luis M. Carril and Walter F. Tichy
Predicting and Witnessing Data Races using CSP

Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Ábrahám, Goran Frehse and Stefan Kowalewski
A Benchmark Suite for Hybrid Systems Reachability Analysis

Jose Divasón and Jesus Aransay-Azofra
Generalizing a Mathematical Analysis library in Isabelle/HOL

Graeme Gange, Jorge A Navas, Peter Schachte, Harald Sondergaard and Peter J Stuckey
A Tool for Intersecting Context-Free Grammars and Its Applications

Reza Hajisheykhi, Ali Ebnenasir and Sandeep Kulkarni
UFIT: A Tool for Modeling Faults in UPPAAL Timed Automata

Marijn Heule, Martina Seidl and Armin Biere
Blocked Literals are Universal

Howard Reubenstein, Greg Eakman, Tom Hawkins, Mitesh Jain and Panagiotis Manolios
Practical Formal Verification of Domain-Specific Language Applications

Olli Saarikivi and Keijo Heljanko
Reporting Races in Dynamic Partial Order Reduction