Matthew B. Dwyer, Rahul Purandare (auth.), Klaus Havelund, Rupak Majumdar, Jens Palsberg (eds.)3540851135, 9783540851134
This book constitutes the refereed proceedings of the 15th International SPIN workshop on Model Checking Software, SPIN 2008, held in Los Angeles, CA, USA, in August 2008.
The 17 revised full papers presented together with 1 tool paper and 4 invited talks were carefully reviewed and selected from 41 submissions. The main focus of the workshop series is software systems, including models and programs. The papers cover theoretical and algorithmic foundations as well as tools for software model checking and foster interactions and exchanges of ideas with related areas in software engineering, such as static analysis, dynamic analysis, and testing.
Table of contents :
Front Matter….Pages –
Residual Checking of Safety Properties….Pages 1-2
The Case for Context-Bounded Verification of Concurrent Programs….Pages 3-6
Combining Static and Dynamic Reasoning for the Discovery of Program Properties….Pages 7-8
Using Dynamic Symbolic Execution to Improve Deductive Verification….Pages 9-25
Automated Evaluation of Secure Route Discovery in MANET Protocols….Pages 26-41
Model Checking Abstract Components within Concrete Software Environments….Pages 42-59
Generating Compact MTBDD-Representations from Probmela Specifications….Pages 60-76
Dynamic Delayed Duplicate Detection for External Memory Model Checking….Pages 77-94
State Focusing: Lazy Abstraction for the Mu-Calculus….Pages 95-113
Efficient Modeling of Concurrent Systems in BMC….Pages 114-133
Tackling Large Verification Problems with the Swarm Tool….Pages 134-143
Formal Verification of a Flash Memory Device Driver – An Experience Report….Pages 144-159
Layered Duplicate Detection in External-Memory Model Checking….Pages 160-175
Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes….Pages 176-195
Improved On-the-Fly Equivalence Checking Using Boolean Equation Systems….Pages 196-213
Resource-Aware Verification Using Randomized Exploration of Large State Spaces….Pages 214-231
Incremental Hashing for Spin ….Pages 232-249
Verifying Compiler Based Refinement of Bluespec TM Specifications Using the SPIN Model Checker….Pages 250-269
Symbolic Context-Bounded Analysis of Multithreaded Java Programs….Pages 270-287
Efficient Stateful Dynamic Partial Order Reduction….Pages 288-305
Symbolic String Verification: An Automata-Based Approach….Pages 306-324
Verifying Multi-threaded C Programs with SPIN….Pages 325-342
Back Matter….Pages –
Reviews
There are no reviews yet.