Proceedings of the 10th SPIN Workshop
Portland, Oregon, USA
Co-located with ICSE 2003
Sponsored by ACM SIGSOFT
May 9 - 10, 2003


Published as:
	Lecture Notes in Computer Science,
	Volume 2648, Springer Verlag, May 2003

Technical Program:

Invited
Talk

Russel, Frege and Spin...
Gerard Holzmann
NASA/JPL, Laboratory for Reliable Software
Session 1
SPIN
Applications

Optimal Scheduling using Branch and Bound with SPIN 4.0 (PDF)
Theo C. Ruys, University of Twente

A Requirements Patterns-Driven Approach to Specify Systems and Check Properties (PDF)
Sascha Konrad, Michigan State University
Laura Campbell, Michigan State University
Betty Cheng, Michigan State University
Min Deng, Michigan State University

Formal Modeling and Analysis of an Avionics Triplex Sensor Voter (PS)
Samar Dajani-Brown, Honeywell
Darren Cofer, Honeywell
Gary Hartmann, Honeywell
Steve Pratt, Honeywell
Session 2
Model
Checking
Algorithms

Distributed Explicit Fair Cycle Detection (PDF)
Ivana Cerna, Faculty of Informatics, Masaryk Universtiy, Brno, Czech Republic
Radek Pelanek, Faculty of Informatics, Masaryk Universtiy, Brno, Czech Republic

Efficient Model Checking of Safety Properties (PDF)
Timo Latvala, Helsinki University of Technology

A Light-weight Algorithm for Model Checking with Symmetry Reduction and Weak Fairness (PDF)
Dragan Bosnacki, Eindhoven University of Technology, The Netherlands
Session 3



A SAT Characterization of Boolean-Program Correctness (PDF)
K. Rustan M. Leino, Microsoft Research

What Went Wrong: Explaining Counterexamples (PDF)
Alex Groce, Carnegie Mellon University
Willem Visser, RIACS/NASA Ames Research Center

A Nearly Memory-optimal Data Structure for Sets and Mappings (PDF)
Jaco Geldenhuys, Institute of Software Systems, Tampere University of Technology
Antti Valmari, Institute of Software Systems, Tampere University of Technology
Invited
Talk

Randomized Algorithms for Program Analysis and Verification
George Necula, UC Berkeley
Session 4
Model
Checking
Applications

Checking Consistency of SDL+MSC specifications (PDF)
Deepak D'Souza, Chennai Mathematical Institute
Madhavan Mukund, Chennai Mathematical Institute

Model Checking Publish-Subscribe Systems (PDF)
David Garlan, Carnegie Mellon University
S. Khersonsky, Carnegie Mellon University
Jung Soo Kim, Carnegie Mellon University

A Methodology for Model-checking Ad-hoc Networks (PDF)
Irfan Zakiuddin, QinetiQ
Michael Goldsmith, Formal Systems (Europe) Ltd.
P. Whittaker
P. Gardiner
Session 5
Tools

Unification and Sharing in Timed Automata Verification (PDF)
Alexandre David, Uppsala University
Gerd Behrmann, Aalborg University
Kim Larsen, Aalborg University
Wang Yi, Uppsala University

The Maude LTL Model Checker and its Implementation (PDF)
Steven Eker, SRI
Jose Meseguer, University of Illinois at Urbana-Champaign
Ambarish Sridharanarayanan, University of Illinois at Urbana-Champaign

Software Verification with Blast (PDF)
Thomas Henzinger, UC Berkeley
Ranjit Jhala, UC Berkeley
Rupak Majumdar, UC Berkeley
Gregoire Sutre, Labri, France
Session 6




Promela Planning (PDF)
Stefan Edelkamp, Institut fuer Informatik

Thread-Modular Model Checking (PDF)
Cormac Flanagan, Systems Research Center, HP Labs
Shaz Qadeer, Microsoft Research

Program Committee

Thomas Ball Microsoft Research co-chair
Matthew Dwyer Kansas State Univ.  
Javier Esparza Univ. Edinburgh  
Kousha Etessami Univ. Edinburgh  
Patrice Godefroid Bell Laboratories  
Susanne Graf VERIMAG  
Somesh Jha Univ. Wisconsin - Madison  
Peter O'Hearn Univ. London  
Andreas Podelski Max Plank Institute  
Sriram Rajamani Microsoft Research co-chair
Mooly Sagiv Tel-Aviv Univ.  
Scott Stoller SUNY Stony Brook  

Spin Homepage
(Page updated: 19 April 2003)