5./6. SPIN 1999: Trento, Italy / Toulouse, France

@proceedings{DBLP:conf/spin/1999,
  editor    = {Dennis Dams and
               Rob Gerth and
               Stefan Leue and
               Mieke Massink},
  title     = {Theoretical and Practical Aspects of SPIN Model Checking, 5th
               and 6th International SPIN Workshops, Trento, Italy, July 5,
               1999, Toulouse, France, September 21 and 24 1999, Proceedings},
  booktitle = {SPIN},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1680},
  year      = {1999},
  isbn      = {3-540-66499-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Part I: Selection of Papers Presented at 5th SPIN99

Keynote Address

• John M. Rushby:
  Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving. 1-11
  Electronic Edition (Springer LINK) BibTeX

Theory

• Jaco Geldenhuys, P. J. A. de Villiers:
  Runtime Efficient State Compaction in SPIN. 12-21
  Electronic Edition (Springer LINK) BibTeX
• Flavio Lerda, Riccardo Sisto:
  Distributed-Memory Model Checking with SPIN. 22-39
  Electronic Edition (Springer LINK) BibTeX
• Dragan Bosnacki:
  Partial Order Reduction in Presence of Rendez-vous Communications with Unless Constructs and Weak Fairness. 40-56
  Electronic Edition (Springer LINK) BibTeX
• Karsten Stahl, Kai Baukus, Yassine Lakhnech, Martin Steffen:
  Divide, Abstract, and Model-Check. 57-76
  Electronic Edition (Springer LINK) BibTeX

Part II: Selection of Papers Presented at 6th SPIN99

Keynote Address

• Dan Craigen:
  Formal Methods Adoption: What's Working, What's Not! 77-91
  Electronic Edition (Springer LINK) BibTeX

Methodology

• Wil Janssen, Radu Mateescu, Sjouke Mauw, Peter Fennema, Petra van der Stappen:
  Model Checking for Managers. 92-107
  Electronic Edition (Springer LINK) BibTeX
• Theo C. Ruys:
  Xspin/Project - Integrated Validation Management for Xspin. 108-119
  Electronic Edition (Springer LINK) BibTeX

Applications I

• Gerald Lüttgen, Victor Carreño:
  Analyzing Mode Confusion via Model Checking. 120-135
  Electronic Edition (Springer LINK) BibTeX
• Carl B. Adekunle, Steve Schneider:
  Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network Using Promela and Xspin. 136-151
  Electronic Edition (Springer LINK) BibTeX
• Klaus Havelund:
  Java PathFinder, A Translator from Java to Promela. 152
  Electronic Edition (Springer LINK) BibTeX
• Moataz Kamel, Stefan Leue:
  VIP: A Visual Interface for Promela. 153
  Electronic Edition (Springer LINK) BibTeX

Specification and Validation

• Marsha Chechik, Dimitrie O. Paun:
  Events in Property Patterns. 154-167
  Electronic Edition (Springer LINK) BibTeX
• Corina S. Pasareanu, Matthew B. Dwyer, Michael Huth:
  Assume-Guarantee Model Checking of Software: A Comparative Case Study. 168-183
  Electronic Edition (Springer LINK) BibTeX
• María-del-Mar Gallardo, Pedro Merino:
  A Framework for Automatic Construction of Abstract Promela Models. 184-199
  Electronic Edition (Springer LINK) BibTeX

Applications II

• Wenhui Zhang:
  Model Checking Operator Procedures. 200-215
  Electronic Edition (Springer LINK) BibTeX
• Klaus Havelund, Jens U. Skakkebæk:
  Applying Model Checking in Java Verification. 216-231
  Electronic Edition (Springer LINK) BibTeX

Extensions

• Gerard J. Holzmann:
  The Engineering of a Model Checker: The Gnu i-Protocol Case Study Revisited. 232-244
  Electronic Edition (Springer LINK) BibTeX
• Heikki Tuominen:
  Embedding a Dialect of SDL in PROMELA. 245-260
  Electronic Edition (Springer LINK) BibTeX
• Claudio Demartini, Radu Iosif, Riccardo Sisto:
  dSPIN: A Dynamic Extension of SPIN. 261-276
  Electronic Edition (Springer LINK) BibTeX