| Invited Talks |
|---|
| [PDF] Proving properties of concurrent C programs,
Gerard Holzmann |
| Conditional model checking,
Dirk Beyer |
| Technical Papers |
|---|
| [PDF] Regression Verification using Impact Summaries,
John Backes, Suzette Person, Neha Rungta and Oksana Tkachuk |
| [PDF] Expression Reduction from Programs in a Symbolic Binary Executor,
Anthony Romano and Dawson Engler |
| [PDF] Property-Driven Benchmark Generation,
Bernhard Steffen, Malte Isberner, Stefan Naujokat, Tiziana Margaria and Maren Geske |
| [PDF] On the Synergy of Probabilistic Causality Computation and Causality Checking,
Florian Leitner-Fischer and Stefan Leue |
| [PDF] On-the-Fly Control Software Synthesis,
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci |
| [PDF] Guard-based Partial Order Reduction,
Alfons Laarman, Elwin Pater and Jaco van de Pol |
| [PDF] Local Model Checking of Weighted CTL with Upper-Bound Constraints,
Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiri Srba and Lars Kaerlund Ostergaard |
| [PDF] Compositional Approach to Suspension and Other Improvements to LTL Translation,
Tomas Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmir Kretinsky and Jan Strejcek |
| [PDF] Automatic Equivalence Checking of UF+IA Programs,
Nuno P. Lopes and Jose Monteiro |
| [PDF] Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms,
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith and Josef Widder |
| [PDF] Spin the Groove: Specification of Link Reversal Routing as Graph Transformations,
Giorgio Delzanno and Riccardo Traverso |
| [PDF] Abstraction-Based Guided Search for Hybrid Systems,
Sergiy Bogomolov, Alexandre Donze, Goran Frehse, Radu Grosu, Taylor T Johnson, Hamed Ladan, Andreas Podelski and Martin Wehrle |
| [PDF] Verifying a Quantitative Relaxation of Linearizability via Refinement,
Kiran Adhikari, James Street, Chao Wang, Yang Liu and Shaojie Zhang |
| [PDF] Model Checking Unbounded Concurrent Lists,
Divjyot Sethi, Murali Talupur and Sharad Malik |
| [PDF] A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software,
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci |
| [PDF] Mining Sequential Patterns to Explain Concurrent Counterexamples,
Stefan Leue and Mitra Tabaei Befrouei |
| [PDF] Error-Completion in Interface Theories,
Stavros Tripakis, Christos Stergiou, Manfred Broy and Edward Lee |
| [PDF] Probabilistic Verification of Coordinated Multi-Robot Missions,
Sagar Chaki and Joseph Giampapa |
| Tool Papers |
|---|
| [PDF] COMPLeTe - A COMmunication Protocol vaLidation Toolchain using Formal and Model-Based Specifications and Descriptions,
Sven Groening, Christopher Rosas and Christian Wietfeld |
| [PDF] Synthesizing Controllers for Automation Tasks with Performance Guarantees,
Chih-Hong Cheng, Michael Geisinger and Christian Buckl |