Model checking software : 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001 : proceedings / Matthew Dwyer (ed.). - Berlin ; New York : Springer, 2001. - 1 online resource (x, 311 pages) : illustrations - Lecture notes in computer science ; 2057 Serienbezeichnung . - Lecture notes in computer science ; 2057. .

On cover: ACM SIGSOFT.

Includes bibliographical references and index.

From model checking to a temporal proof / Model checking if your life depends on it: a view from intel's trenches / Model-checking infinite state-space systems with fine-grained abstractions using SPIN / Implementing LTL model checking with net unfoldings / Directed explicit model checking with HSF-SPIN / Addressing dynamic issues of program model checking / Automaticallu validating temporal safety properties of interfaces / Verification experiments on the MASCARA protocol / Using SPIN for feature interaction analysis-a case study / Behavioural analysis of the enterprise javabens component architecture / p2b: a translation utility for linking promela and symbolic model checking (tool paper) / Transformations for model checking distributed java programs / Distribured LTL model-checking in SPIN / Parallel state space construction for model-checking / Model checking systems of replicated processes with spin / SPIN-based model checker for telecommunication protocols / Modeling and verifying a price model for congestion control in computer networks using promela/spin / Model checking project at philips research / Applications of model checking at honeywell laboratories / Coarse-granular model checking in practice / Doron Peled, Lenore Zuck -- Rob Gerth -- Marsha Chechik, Bebet Devereux, Arie Gurfinkel -- Javier Esparza, Keijo Heljanko -- Stefan Edelkamp, Alberto Lluch-Lafuente, Stefan Leue -- Flavio Lerda, Willem Visser -- Thomas Ball, Sriram K. Rajamani -- Guoping Jia, Susanne Graf -- Muffy Calder, Alice Miller -- Shin Nakajima, Tetsuo tamai -- Michael Baldamus, Jochen Schröder-Babo -- Scott D. Stoller, Yanhong A. Liu -- Jiri Barnat, Lubos Brim, Jitka Stříbrná -- Hubert Garavel, Radu Mateescu, Irina Smarandache -- Fabrice derepas, Paul Gastin -- Vivek K. Shanbhag, K. Gopinath -- Clement Yuen, Wei Tjioe -- Leszek Holenderski -- Darren Cofer [and others] -- Bernhard Steffen, Tiziana Margaria, Volker Braun.

This book constitutes the refereed proceedings of the 8th International SPIN Workshop held in Toronto, Canada, in May 2001. The SPIN model checker is one of the most powerful and popular systems for the analysis and verification of distributed and concurrent systems. The 13 revised full papers presented together with one invited survey paper and three invited industrial experience reports were carefully reviewed and selected from 26 submissions. Besides foundational issues of program analysis and formal verification, the papers focus on tools for model checking and practical applications in a variety of fields.

9783540451396 3540451390

10.1007/3-540-45139-0 doi

SPIN (Computer file)--Congresses.
SPIN (Computer file)

Computer software--Verification--Congresses.
Computer software--Verification.

Electronic books.
Conference papers and proceedings.

QA76.76.V47 / I58 2001


Powered by Koha