Full Papers
- Matthieu Renard, Antoine Rollet and Ylies Falcone. Runtime Enforcement Using Büchi Games
- Daniel Ratiu and Andreas Ulrich. Increasing Usability of Spin-based C Code Verification Using a Harness Definition Language
- Srinivas Pinisetty, Partha Roop, Steven Smyth, Stavros Tripakis and Reinhard von Hanxleden. Runtime enforcement of reactive systems using synchronous enforcers
- Wytse Oortwijn, Tom van Dijk and Jaco van de Pol. Distributed Binary Decision Diagrams for Symbolic Reachability
- Heila Botha, Oksana Tkachuk, Brink Van Der Merwe and Willem Visser. Addressing Challenges In Obtaining High Coverage When Model Checking Android Applications
- Guangyuan Li, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay and Danny Bøgsted Poulsen. Practical Controller Synthesis for MTL_{0,\infty}
- John Fearnley, Sanjay Jain, Sven Schewe, Frank Stephan and Dominik Wojtczak. An Ordered Approach to Solving Parity Games in Quasi Polynomial Time and Quasi Linear Space
- Thomas Geffroy, Jérôme Leroux and Grégoire Sutre. Backward Coverability with Pruning for Lossy Channel Systems
- Paul Fiterau-Brostean, Frits Vaandrager, Erik Poll, Joeri de Ruiter, Toon Lenaerts and Patrick Verleg. Model Learning and Model Checking of SSH Implementations
- Michalis Kokologiannakis and Konstantinos Sagonas. Stateless Model Checking of the Linux Kernel’s Hierarchical Read-Copy-Update (Tree RCU)
- Idress Husien, Nicolas Berthier and Sven Schewe. A Hot Method for Synthesising Cool Controllers
- Huu Vu Nguyen and Tayssir Touili. CARET Model Checking for Malware Detection
- Jinru Hua and Sarfraz Khurshid. Sketch4J: Execution-Driven Sketching for Java
- Nima Dini, Cagdas Yelen and Sarfraz Khurshid. Optimizing Parallel Korat Using Invalid Ranges
- Pouria Mellati, Ehsan Khamespanah and Ramtin Khosravi. LeeTL: LTL with Quantifications Over Model Objects
- Vincent Bloemen, Alexandre Duret-Lutz and Jaco van de Pol. Explicit State Model Checking with Generalized Büchi and Rabin Automata
Short Papers
- Lucas Wagner, David Greve and Andrew Gacek. SIMPAL: A Compositional Reasoning Framework for Imperative Programs
- Marco Antonio Feliu Gabaldon, Camilo Rocha and Swee Balachandran. Verification-driven Development of Icarous Based on Automatic Reachability Analysis
- Blake Loring, Duncan Mitchell and Johannes Kinder. ExpoSE: Practical Symbolic Execution of Standalone JavaScript
- Laura Panizo, Alberto Salmerón, Maria Del Mar Gallardo and Pedro Merino. Guided Test Case Generation for Mobile Apps in the TRIANGLE Project
- Marcello M. Bersani, Madalina Erascu, Francesco Marconi, Silvio Ghilardi and Matteo Rossi. Formal Verification of Data-Intensive Applications through Model Checking Modulo Theories