Model Checking Software: 18th International SPIN Workshop, Snowbird, UT, USA, July 14-15, 2011. Proceedings

✍ Scribed by Jasmin Fisher (auth.), Alex Groce, Madanlal Musuvathi (eds.)

• Publisher: Springer-Verlag Berlin Heidelberg
• Year: 2011
• Tongue: English
• Leaves: 206
• Series: Lecture Notes in Computer Science 6823
• Edition: 1
• Category: Library

✦ Synopsis

This book constitutes the refereed proceedings of the 18th International SPIN workshop on Model Checking Software, SPIN 2011, held in Snowbird, UT, USA, in July 2011.

The 10 revised full papers presented together with 2 tool demonstration papers and 1 invited contribution were carefully reviewed and selected from 29 submissions. The papers are organized in topical sections on abstractions and state-space reductions; search strategies; PROMELA encodings and extensions; and applications of model checking.

✦ Table of Contents

Front Matter....Pages -
Model Checking Cell Fate Decisions....Pages 1-1
Property-Dependent Reductions for the Modal Mu-Calculus....Pages 2-19
String Abstractions for String Verification....Pages 20-37
Parallel Recursive State Compression for Free....Pages 38-56
Depth Bounded Explicit-State Model Checking....Pages 57-74
Randomized Backtracking in State Space Traversal....Pages 75-89
An Analytic Evaluation of SystemC Encodings in Promela....Pages 90-107
Building Extensible Specifications and Implementations of Promela with AbleP....Pages 108-125
Program Sketching via CTL* Model Checking....Pages 126-143
A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems....Pages 144-160
Model Checking Industrial Robot Systems....Pages 161-176
EpiSpin: An Eclipse Plug-In for Promela/Spin Using Spoofax....Pages 177-182
DiPro - A Tool for Probabilistic Counterexample Generation....Pages 183-187
dBug: Systematic Testing of Unmodified Distributed and Multi-threaded Systems....Pages 188-193
Back Matter....Pages -

✦ Subjects

Software Engineering; Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs; Mathematical Logic and Formal Languages