Proceedings of the 12th SPIN Workshop on Model Checking Software
San Francisco, USA
Co-located with CONCUR 2005
August 22 - 24, 2005

Invited Speakers:

• Rajeev Alur (Univ. Pennsylvania), joint speaker with Concur.
• Dawson Engler (Stanford), joint speaker with Concur.
• David Wagner (UC Berkeley), joint speaker with SecCo.

Technical Program:

Session 1 -- State Representation and Abstraction

• An Incremental Heap Canonicalization Algorithm (PDF)
  Madanlal Musuvathi (Microsoft Research) and David L. Dill (Stanford Univ.)
• Memory Efficient State Space Storage in Explicit Software Model Checking (PDF)
  Sami Evangelista and Jean-Francois Pradat-Peyre (CEDRIC CNAM, Paris, France)
• Counterexample-based Refinement for a Boundedness Test for CFSM Languages (PDF)
  Stefan Leue and Wei Wei (Univ. Konstanz, Germany)

Session 2 -- Dealing with Concurrency

Symbolic Model Checking for Asynchronous Boolean Programs (PDF)
Byron Cook (Microsoft Research), Daniel Kroening (ETH Zurich) and Natasha Sharygina (CMU)
• Improving Spin's Partial Order Reduction for Breadth First Search (PDF)
  Dragan Bosnacki (Eindhoven Univ., The Netherlands), and Gerard J. Holzmann (NASA/JPL)
• Sound Transaction-based Reduction without Cycle Detection (PDF)
  Vladimir Levin (Microsoft), Robert Palmer (Univ. Utah), Shaz Qadeer and Sriram K. Rajamani (Microsoft Reseach)

Tutorial 1

• Effective Bug Hunting with Spin and Modex (PDF)
  by Gerard J. Holzmann (NASA/JPL) and Theo C. Ruys (Univ. Twente, The Netherlands)

Session 3 -- Dealing with Complex Data

• Repairing Structurally Complex Data (PDF)
  Sarfraz Khurshid, Ivan Garcia and Yuk Lai Suen (Univ. of Texas at Austin)
• Crafting a Promela Front-End with Abstract Data Types to Mitigate the Sensitivity of (Compositional) Analysis to Implementation Choices (PDF)
  Yung-Pin Cheng (Nat. Taiwan Normal Univ.)
• Behavioural Models for Hierarchical Components (PDF)
  Tomas Barros, Ludovic Henrio and Eric Madelaine (INRIA Sophia, France)

Session 4 -- Tool Presentations

• ETCH: An Enhanced Type Checking Tool for Promela (PDF)
  Alastair F. Donaldson and Simon J. Gay (Univ. Glasgow, Scotland)
• Enhanced Probabilistic Verification with 3Spin and 3Murphi (PDF)
  Peter C. Dillinger and Panagiotis Manolios (Georgia Inst. of Techn.)
• SPLAT: A Tool for Model-Checking and Dynamically-Enforcing Abstractions (PDF)
  Anil Madhavapeddy (Univ. Cambridge, UK), David Scott (Fraser Research) and Richard Sharp (Intel Research Cambridge, UK)
• Learning-Based Assume-Guarantee Verification (PDF)
  Dimitra Giannakopoulou and Corina S. Pasareanu (NASA Ames Research Center)

Tutorial 2

• The BLAST Software Verification System
  by Tom Henzinger (EPFL Lausanne), Ranjit Jhala (UCSD), Rupak Majumdar (UC Berkeley)

Session 5 -- Checking Temporal Properties

• On-the-fly Emptiness Checks for Generalized Buchi Automata (PDF)
  Jean-Michel Couvreur (Univ. Bordeaux, France), Alexandre Duret-Lutz and Denis Poitrenaud (Univ. Paris, France)
• Stuttering Congruence for Chi (PDF)
  Bas Luttik and Nikola Trcka (Eindhoven Univ., The Netherlands)
• Verifying Pattern-Generated LTL Formulas: A Case Study (PDF)
  Salamah Salamah (Univ. Texas at El Paso), Ann Gates, Steve Roach and Oscar Mondragon (ESI Center, Mexico)

Session 6 -- Checking Security and Real-Time Properties

• Generic Verification of Security Protocols (PDF)
  Abdul Sahid Khan, Madhavan Mukund and S. P. Suresh (Chennai Math. Institute, India)
• Using SPIN and Eclipse for Optimized High-Level Modeling and Analysis of Computer Network Attack Models (PDF)
  Gerrit Rothmaier (Materna GmbH, Dortmund, Germany), Tobias Kneiphoff (Bosch, Germany) and Heiko Krumm (Univ. Dortmund, Germany)
• Model Checking Machine Code with the GNU Debugger (PDF)
  Eric Mercer and Michael Jones (Brigham Young Univ., Utah)

Tutorial 3

• Model Checking Programs with Java PathFinder
  by Willem Visser and Peter Mehlitz (NASA Ames Research Center)