International SPIN Symposium
on Model Checking of Software
on Model Checking of Software
Stony Brook, NY, USA, 8-9 July 2013
Marking the 20th Anniversary of the International SPIN Workshop
For those of you interested in game theory, you can extend your stay at Stony Brook to hear about the latest developments in this field from leading experts.
The provisional program for SPIN 2013 is as follows.
| 8.30 | Registration |
| 9.00 9.15 |
Welcome, Opening Remarks Invited talk: Gerard Holzmann Proving properties of concurrent C programs |
| 10.15 | Coffee Break |
| 10.45 |
Testing Regression Verification using Impact Summaries John Backes, Suzette Person, Neha Rungta and Oksana Tkachuk Expression Reduction from Programs in a Symbolic Binary Executor Anthony Romano and Dawson Engler Property-Driven Benchmark Generation Bernhard Steffen, Malte Isberner, Stefan Naujokat, Tiziana Margaria and Maren Geske |
| 12.15 |
Tool Presentation COMPLeTe - A COMmunication Protocol vaLidation Toolchain using Formal and Model-Based Specifications and Descriptions (Tool paper) Sven Groening, Christopher Rosas and Christian Wietfeld |
| 12.30 | Lunch |
| 14.00 |
Probabilistic Verification and Synthesis Probabilistic Verification of Coordinated Multi-Robot Missions Sagar Chaki and Joseph Giampapa On the Synergy of Probabilistic Causality Computation and Causality Checking Florian Leitner-Fischer and Stefan Leue On-the-Fly Control Software Synthesis Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci |
| 15.30 |
Tool Presentation Synthesizing Controllers for Automation Tasks with Performance Guarantees (Tool Paper) Chih-Hong Cheng, Michael Geisinger and Christian Buckl |
| 15.45 | Coffee Break |
| 16.15 |
Model Checking - 1 Guard-based Partial Order Reduction Alfons Laarman, Elwin Pater and Jaco van de Pol Local Model Checking of Weighted CTL with Upper-Bound Constraints Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiri Srba and Lars Kærlund Østergaard Compositional Approach to Suspension and Other Improvements to LTL Translation Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmir Kretinsky and Jan Strejcek |
| 17.45 | Close |
| 18:30-22:00 | Symposium Banquet |
| 9.00 |
Invited talk: Dirk Beyer Conditional Model Checking |
| 10.00 | Coffee Break |
| 10.30 |
Model Checking - 2 Automatic Equivalence Checking of UF+IA Programs Nuno P. Lopes and Jose Monteiro Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith and Josef Widder Spin the Groove: Specification of Link Reversal Routing as Graph Transformations Giorgio Delzanno and Riccardo Traverso |
| 12.00 | Lunch Break (SCGP Cafe) |
| 14.00 |
Abstraction and Refinement Abstraction-Based Guided Search for Hybrid Systems Sergiy Bogomolov, Alexandre Donzé, Goran Frehse, Radu Grosu, Taylor T Johnson, Hamed Ladan, Andreas Podelski and Martin Wehrle Verifying a Quantitative Relaxation of Linearizability via Refinement Kiran Adhikari, James Street, Chao Wang, Yang Liu and Shaojie Zhang Model Checking Unbounded Concurrent Lists Divjyot Sethi, Murali Talupur and Sharad Malik |
| 15:30 | Coffee Break |
| 16:00 |
Debugging and Synthesis A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo and Enrico Tronci Mining Sequential Patterns to Explain Concurrent Counterexamples Stefan Leue and Mitra Tabaei Befrouei Error-Completion in Interface Theories Stavros Tripakis, Christos Stergiou, Manfred Broy and Edward Lee |
| 17:30 | Close |
|
|
|
|
|