Model Checking Software: 8th International SPIN Workshop Toronto, Canada, May 19–20, 2001 Proceedings

From model checking to a temporal proof....Pages 1-14
Model checking if your life depends on it: a view from intel’s trenches....Pages 15-15
Model-checking in finite state-space systems with fine-grained abstractions using SPIN....Pages 16-36
Implementing LTL model checking with net unfoldings....Pages 37-56
Directed explicit model checking with HSF-SPIN....Pages 57-79
Addressing dynamic issues of program model checking....Pages 80-102
Automatically validating temporal safety properties of interfaces....Pages 102-122
Verification experiments on the MASCARA protocol....Pages 123-142
Using SPIN for feature interaction analysis - a case study....Pages 143-162
Behavioural analysis of the enterprise javaBeans ™ component architecture....Pages 163-182
p2b: A translation utility for linking promela and symbolic model checking (tool paper)....Pages 183-191
Transformations for model checking distributed java programs....Pages 192-199
Distributed LTL model-checking in SPIN....Pages 200-216
Parallel state space construction for model-checking....Pages 217-234
Model checking systems of replicated processes with spin....Pages 235-251
A SPIN-based model checker for telecommunication protocols....Pages 252-271
Modeling and verifying a price model for congestion control in computer networks using promela/spin....Pages 272-287
A model checking project at philips research....Pages 288-295
Applications of model checking at honeywell laboratories....Pages 296-303
Coarse-granular model checking in practice....Pages 304-311