SPIN 2013 Program, July 8-9, 2013, Stony Brook, NY

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

Spin Homepage
Spin Workshops