Proceedings of the 7th SPIN Workshop
Stanford University, California

Held: August 30 - September 1, 2000

Published as:
	Lecture Notes in Computer Science,
	Volume 1885, Springer Verlag.
	September 2000, ISSN 0302-9743.
	The page numbers below refer to this publication.

• Leslie Lamport (Compaq Systems Research Center)
  Model Checking Specifications
• Peter Gluck (NASA/JPL Jet Propulsion Laboratory)
  Debugging, Testing and Verification of the Deep-Space 1 Spacecraft Software

• Doron Drusinsky (Time Rover Inc.)
  Temporal Rover (pp. 323-330, PDF)
• Philippa Broadfoot for Bill Roscoe (Oxford University Computing Laboratory)
  The FDR model checker (pp 322-322, PDF)
• Jim Saxe (Compaq Systems Research)
  The Extended Static Checker (ESC)
• Jerry Harrow (Compaq)
  Visual Threads (pp. 331-342, PDF)

• Symmetric Spin, D. Bosnacki, D. Dams, and L. Holenderski, Eindhoven University, The Netherlands. (pp. 1-19, PDF)
• Using Garbage Collection in Model Checking, R. Iosif and R. Sisto, Politecnico di Torino, Italy. (pp. 20-33, PDF)
• Model Checking Based on Simultaneous Reachability Analysis, B. Karacali and K. C. Tai, North-Carolina State University. (pp. 34-53, PDF)
• Testing SPIN's LTL Formula Conversion into Buchi Automata with Randomly Generated Input, H. Tauriainen and K. Heljanko, Helsinki University, Finland. (pp. 54-72, PDF)
• Verification and Optimization of a PLC Control Schedule, E. Brinksma and A. Mader, Twente University, The Netherlands (pp. 73-92, PDF)
• Modeling the ASCB-D Synchronization Algorithm with SPIN: A Case Study, N. Weininger and D. Cofer, Honeywell Technology Center, Minneapolis. (pp. 93-112, PDF)
• Bebop: A Symbolic Model Checker for Boolean Programs, T. Ball and S. K. Rajamani, Microsoft Research. (pp. 113-130, PDF)
• Logic Verification of ANSI C Code with SPIN, G.J. Holzmann, Bell Laboratories. (pp. 131-147, PDF)
• Interaction Abstraction for Compositional Finite State Systems, W. Liu, University of Waterloo, Canada. (pp. 148-162, PDF)
• Correctness by Construction: Towards Verification in Hierarchical System Development, M. Majster-Cederbaum and F. Salger, Univ. of Mannheim, Germany. (pp. 163-180, PDF)
• Linking STEP with SPIN, A. Browne, H. Sipma and T. Zhang, Stanford University. (pp. 181-186, PDF)
• Abstraction of Communication Channels in Promela: a Case Study, E. Fersman and B. Jonsson, University Uppsala, Sweden. (pp. 187-204, PDF)
• A Language Framework for Expressing Checkable Properties of Dynamic Software, J. Corbett, M. Dwyer, J. Hatcliff, and Robby, Univ. of Hawaii, and Kansas State University. (pp. 205-223, PDF)
• Model-Checking Multi-Threaded Distributed Java Programs, S. D. Stoller, Indiana University, Bloomington, IN. (pp. 224-244, PDF)
• Using Runtime Analysis to Guide Model Checking of Java Programs, K. Havelund, NASA Ames Research Center, Moffet Field, California. (pp. 245-264, PDF)
• Communication Topology Analysis for Concurrent Programs, M. Martel and M. Gengler, Lab. d'Informatique de Marseille, France. (pp. 265-286, PDF)
• Low-Fat Recipes for SPIN, T. C. Ruys, Twente University, The Netherlands. (pp. 287-321, PDF)