Model Checking Software: 12th International SPIN Workshop模型检验软件/会议录

This book constitutes the refereed proceedings of the 12th International SPIN workshop on Model Checking Software, SPIN 2005, held in San Francisco, USA in August 2005.
　　The 15 revised full papers presented were carefully reviewed and selected from 45 submissions; in addition there are 4 tool presentation papers selected from 6 submissions. The papers are organized in topical sections on state representation and abstraction, dealing with concurrency, dealing with complex data, checking temporal properties, and checking security and real-time properties

Invited Talks/Papers
　Pushdown Model Checking for Security
　Execution Generated Test Cases：How to Make Systems Code Crash Itsel
Invited Tutorials
　Effective Bug Hunting with Spin and Modex
　The BLAST Software Verification System
　Model Checking Programs with Java PathFinder
State Representation and Abstraction
　An Incremental Heap Canonicalization Algorithm
　Memory Efficient State Space Storage in Explicit Software Model Checking
　Counterexample—Based Refinement for a Boundedness Test for CFSM Languages
Dealing with C0ncurrency
　Symbolic Model Checking for Asynchronous Boolean Programs
　Improving Spin’S Partial—Order Reduction for Breadth—First Search
　Sound Transaction—Based Reduction Without Cycle Detection
Dealing with Complex Data
　Repairing Structurally Complex Data
　Crafting a Promela Front—End with Abstract Data Types to Mitigate the Sensitivity of(Compositional)Analysis to Implementation Choices
　Behavioural Models for Hierarchical Components
Checking Temporal Properties
On-the-fly Emptiness Checks for Generalized Biichi Automata
Stuttering Congruence for)(
Verifying Pattern—Generated LTL Formulas：A Case Study
Checking Security and Real—Time Properties
Generic Verification of Security Protocols
Using SPIN and Eclipse for Optimized High—Level Modeling and Analysis of Computer Network Attack Models
Model Checking Machine Code with the GNU Debugger
Tool Papers
Author Index