This book constitutes the refereed proceedings of the 14th International SPIN workshop on Model Checking Software, SPIN 2007, held in Berlin, Germany in July 2007 in conjunction with the 19th International Conference on Computer Aided Verification, CAV 2007.
The 14 revised full papers presented together with 4 tool presentation papers and the abstracts of 2 invited talks were carefully reviewed and selected from 39 submissions. The papers are organized in topical sections on directed model checking, partial order reduction, program analysis, exploration advances, modeling and case studies, as well as tool demonstrations.
Author(s): Dennis Dams (auth.), Dragan Bošnački, Stefan Edelkamp (eds.)
Series: Lecture Notes in Computer Science 4595
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2007
Language: English
Pages: 285
Tags: Software Engineering; Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs
Front Matter....Pages -
StackSnuffer: Curing Orion’s Unsoundness....Pages 1-1
Tutorial: Parallel Model Checking....Pages 2-3
Local Abstraction-Refinement for the mu-Calculus....Pages 4-23
Minimal Counterexample Generation for SPIN....Pages 24-38
Generating Counter-Examples Through Randomized Guided Search....Pages 39-57
Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software....Pages 58-75
Some Solutions to the Ignoring Problem....Pages 76-94
Cartesian Partial-Order Reduction....Pages 95-112
On-the-Fly Dynamic Dead Variable Analysis....Pages 113-130
SAT-Based Summarization for Boolean Programs....Pages 131-148
LTL Satisfiability Checking....Pages 149-167
An Embeddable Virtual Machine for State Space Generation....Pages 168-186
Scalable Multi-core LTL Model-Checking....Pages 187-203
A SystemC/TLM Semantics in Promela and Its Possible Applications....Pages 204-222
Towards Model Checking Spatial Properties with SPIN ....Pages 223-242
Model Extraction for ARINC 653 Based Avionics Software....Pages 243-262
BEEM: Benchmarks for Explicit Model Checkers....Pages 263-267
C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs....Pages 268-273
ACSAR: Software Model Checking with Transfinite Refinement....Pages 274-278
Instrumenting C Programs with Nested Word Monitors....Pages 279-283
Back Matter....Pages -
