SPIN 2011 Program

July 14: Thursday
7:00-8:30Breakfast
8:45-8:55
SPIN Welcome
Alex Groce, Madan Musuvathi
9:00-10:00
Invited Speaker
Tom Ball, Microsoft Research
A Tool Based Approach to Conquering Concurrent Programming
(Jointly with EC2)
10:00-10:30 Coffee
10:30-12:00
Abstractions and State-Space Reductions (Chair: Stefan Leue)
Property-Dependent Reductions for the Modal Mu-Calculus
Radu Mateescu and Anton Wijs
String Abstractions for String Verification
Fang Yu, Tevfik Bultan and Ben Hardekopf
Parallel Recursive State Compression for Free
Alfons Laarman, Jaco Van De Pol and Michael Weber
12:00-1:30 Sack Lunch
1:30-3:00
Applications of Model Checking (Chair: Shaz Qadeer)
Program Sketching via CTL* Model Checking
Andreas Morgenstern and Klaus Schneider
A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems
Alexander Linden and Pierre Wolper
Model Checking Industrial Robot Systems
Markus Weissmann, Stefan Bedenk, Christian Buckl and Alois Knoll
3:00-3:30 Coffee
3:30-4:30
Invited Speaker (Chair: Madan Musuvathi)
Jasmin Fisher, Microsoft Research
Model Checking Cell Fate Decisions
July 15: Friday
7:00-8:30Breakfast
9:00-10:00
Invited Speaker (Chair: Alex Groce)
John Regehr, University of Utah
Random Testing for C Compilers
10:00-10:30 Coffee
10:30-11:30
Search Strategies (Chair: Murali Talupur)
Depth Bounded Explicit State Model Checking
Abhishek Udupa, Ankush Desai and Sriram Rajamani
Randomized Backtracking in State Space Traversal
Pavel Parizek and Ondrej Lhotak
11:30-12:00
PROMELA Encodings and Extensions - I
An Analytic Evaluation of SystemC Encodings in Promela
Daniele Campana, Alessandro Cimatti, Iman Narasamdya and Marco Roveri
12:00-1:30 Sack Lunch
1:30-2:00
PROMELA Encodings and Extensions - II (Chair: Madan Musuvathi)
Building Extensible Specifications and Implementations of Promela with AbleP
Yogesh Mali and Eric Van Wyk
2:00-3:00
Invited Speaker
Murali Talupur, Intel
Reasoning About Replication: Parameteric Verification of Industrial Protocols
(Jointly with EC2)
3:00-3:30 Coffee
3:30-4:30
Tool Demonstrations (Chair: Alex Groce)
EpiSpin: en Eclipse Plug-in for Promela/Spin using Spoofax.
Bob De Vos, Lennart Kats and Cornelis Pronk
DiPro - A Tool for Probabilistic Counterexample Generation
Husain Aljazzar, Florian Leitner-Fischer, Stefan Leue and Dimitar Simeonov
dBug: Systematic Testing of Unmodified Distributed and Multi-Threaded Systems
Jiri Simsa, Randy Bryant and Garth Gibson