Model checking software : 8th International SPIN Workshop, Toronto, Canada, May 19-20, 2001 : proceedings / Matthew Dwyer (ed.).
Contributor(s): Dwyer, Matthew | ACM SigsoftMaterial type: TextSeries: SerienbezeichnungLecture notes in computer science: 2057.Publisher: Berlin ; New York : Springer, 2001Description: 1 online resource (x, 311 pages) : illustrationsContent type: text Media type: computer Carrier type: online resourceISBN: 9783540451396; 3540451390Subject(s): SPIN (Computer file) -- Congresses | SPIN (Computer file) | Computer software -- Verification -- Congresses | Computer software -- VerificationGenre/Form: Electronic books. | Conference papers and proceedings. Additional physical formats: Print version:International SPIN Workshop (8th : 2001 Toronto, Ont.).: Model checking software.DDC classification: 005.1/4 LOC classification: QA76.76.V47 | I58 2001Online resources: Click here to access online
|Item type||Current location||Collection||Call number||Status||Date due||Barcode||Item holds|
On cover: ACM SIGSOFT.
Includes bibliographical references and index.
From model checking to a temporal proof / Doron Peled, Lenore Zuck -- Model checking if your life depends on it: a view from intel's trenches / Rob Gerth -- Model-checking infinite state-space systems with fine-grained abstractions using SPIN / Marsha Chechik, Bebet Devereux, Arie Gurfinkel -- Implementing LTL model checking with net unfoldings / Javier Esparza, Keijo Heljanko -- Directed explicit model checking with HSF-SPIN / Stefan Edelkamp, Alberto Lluch-Lafuente, Stefan Leue -- Addressing dynamic issues of program model checking / Flavio Lerda, Willem Visser -- Automaticallu validating temporal safety properties of interfaces / Thomas Ball, Sriram K. Rajamani -- Verification experiments on the MASCARA protocol / Guoping Jia, Susanne Graf -- Using SPIN for feature interaction analysis-a case study / Muffy Calder, Alice Miller -- Behavioural analysis of the enterprise javabens component architecture / Shin Nakajima, Tetsuo tamai -- p2b: a translation utility for linking promela and symbolic model checking (tool paper) / Michael Baldamus, Jochen Schröder-Babo -- Transformations for model checking distributed java programs / Scott D. Stoller, Yanhong A. Liu -- Distribured LTL model-checking in SPIN / Jiri Barnat, Lubos Brim, Jitka Stříbrná -- Parallel state space construction for model-checking / Hubert Garavel, Radu Mateescu, Irina Smarandache -- Model checking systems of replicated processes with spin / Fabrice derepas, Paul Gastin -- SPIN-based model checker for telecommunication protocols / Vivek K. Shanbhag, K. Gopinath -- Modeling and verifying a price model for congestion control in computer networks using promela/spin / Clement Yuen, Wei Tjioe -- Model checking project at philips research / Leszek Holenderski -- Applications of model checking at honeywell laboratories / Darren Cofer [and others] -- Coarse-granular model checking in practice / 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.