Proceedings of the 9th SPIN Workshop
Grenoble, France

Held: April 11 - 13, 2002

Published as:
	Lecture Notes in Computer Science,
	Volume 2318, Springer Verlag.
	April 2002, ISSN 0302-9743, ISBN 3-540-43477-1
	The page numbers below refer to this publication.

• Edmund M. Clarke (CMU), SAT-Based counterexample guided abstraction refinement
• Patrick Cousot (ENS), Abstract Interpretation: theory and practice

• Theo Ruys (Univ. of Twente), SPIN Tutorial: how to become a SPIN Doctor
  (pp. 6-13, PDF) (vugraphs)
• Dennis Dams (Bell Labs), Abstraction in software model checking: principles and practice
  (vugraphs, 3.4 Mb)

• Symmetry Reduction Criteria for Software Model Checking, R. Iosif (Kansas State University)
  (pp. 22-41, PDF)
• Bytecode Model Checking: An Experimental Analysis, D. Basin, S. Friedrich, M. Gawkowski (Freiburg University) and J. Posegga (SAP AG, Corporate Research, Karlsruhe)
  (pp. 42-59, PDF)
• The Influence of Software Module Systems on Modular Verification, H. Li (Brown University), K. Fisler (Worcester Polytechnic Institute) and S. Krishnamurthi (Brown University)
  (pp. 60-78, PDF)
• Extending the Translation from SDL to Promela, A. Prigent (ENSIETA, Brest), F. Cassez (IRCCyN, ECN, Nantes), P. Dhaussy (ENSIETA, Brest) and O. Roux (IRCCyN, ECN, Nantes)
  (pp. 79-94, PDF)
• Model Checking Knowledge and Time, W. van der Hoek (Utrecht University) and M. Woolridge (University of Liverpool)
  (pp. 95-111, PDF)
• Partial Order Reduction in Directed Model Checking, A. Lluch-Lafuente, S. Edelkamp and S. Leue (Albert Ludwig Univeristy, Freiburg)
  (pp. 112-127, PDF)
• Parallel Model Checking for the Alternation-Free mu-Calculus, B. Bollig (RWTH Aachen), M. Leucker (University of Pensylvania) and M. Weber (RWTH Aachen)
  (pp. 128-147, PDF)
• The Agreement Problem Protocol Verification Environment, J. Pascoe, R. J. Loader (The University of Reading) and V. S. Sunderam (Emory University, Atlanta)
  (pp. 148-169, PDF)
• Bottleneck Analysis of a Gigabit Network Interface Card: A Formal Verification Approach, H. Jin, K. Bang, C. Yoo, J. Choi (Korea University, Seoul)
  (pp. 170-186, PDF)
• Using SPIN to verify security properties of cryptographic protocols, P. Maggi and R. Sisto (Politecnico di Torino)
  (pp. 187-204, PDF)
• Heuristic Model Checking for Java Programs, A. Groce (Carnegie Mellon University), W. Visser (RIACS/NASA Ames Research Center)
  (pp. 242-245, PDF)
• System Specification and Verification Using High Level Concepts, C. Stehno (Carl von Ossietzky University Oldenburg)
  (pp. 246-249, PDF)
• Demonstration of an Automated Integrated Test Environment for Web-based Applications, T. Margaria (Metaframe Technologies and University of Dortmund), O. Niese, B. Steffen (University of Dortmund)
  (pp. 250-253, PDF)
• aSPIN: Extending SPIN with Abstraction, P. Merino, M. del Mar Gallardo, J. Martinez, E. Pimentel (University of Malaga)
  (pp. 254-258, PDF)

• Modeling and Verification of Interactive Flexible Multimedia Presentations Using PROMELA/SPIN, R. S. Aygun, A. Zhang (State University of New York, Buffalo)
  (pp. 205-212, PDF)
• SPINning Parallel Systems Software, O. Shumsky Matlin, E. Lusk, W. McCune (Argonne National Laboratory, Argonne)
  (pp. 213-220, PDF)
• Dynamic Bounds and Transition Merging for Local First Search, P. Niebert, D. Lugiez, S. Zennou (Laboratoire d'Informatique Fondamentale, Marseille)
  (pp. 212-229, PDF)

• Cindy Eisner (IBM), Comparing symbolic and explicit model checking
• Per Bjesse (Prover Technology), Industrial model checking based on satisfiability solvers
• Yves-Marie Quemener (France Telecom), A typical testing problem: validating WML cellphones