This book constitutes the refereed proceedings of the 17th International SPIN workshop on Model Checking Software, SPIN 2010, held at the University of Twente, in Enschede, The Netherlands, in September 2010. The 13 revised full papers presented together with 2 tool papers and 3 invited talks were carefully reviewed and selected from 33 submissions. The papers are organized in topical sections on satisfiability modulo theories for model checking, model checking in context (simulation, testing, UML), implementation and performance of model checking, LTL and Büchi automata, extensions to infinite-state systems, and concurrent software.
Author(s): Alessandro Cimatti (auth.), Jaco van de Pol, Michael Weber (eds.)
Series: Lecture Notes in Computer Science 6349 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2010
Language: English
Pages: 263
Tags: Software Engineering; Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs; Mathematical Logic and Formal Languages
Front Matter....Pages -
SMT-Based Software Model Checking....Pages 1-3
Symbolic Object Code Analysis....Pages 4-21
Experimental Comparison of Concolic and Random Testing for Java Card Applets....Pages 22-39
Combining SPIN with ns-2 for Protocol Optimization....Pages 40-57
Automatic Generation of Model Checking Scripts Based on Environment Modeling....Pages 58-75
Model Checking: Cleared for Take Off....Pages 76-87
Context-Enhanced Directed Model Checking....Pages 88-105
Efficient Explicit-State Model Checking on General Purpose Graphics Processors....Pages 106-123
The SpinJa Model Checker....Pages 124-128
On the Virtue of Patience: Minimizing Büchi Automata....Pages 129-145
Enacting Declarative Languages Using LTL: Avoiding Errors and Improving Performance....Pages 146-161
Nevertrace Claims for Model Checking....Pages 162-179
A False History of True Concurrency: From Petri to Tools....Pages 180-186
Analysing Mu-Calculus Properties of Pushdown Systems....Pages 187-192
Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains....Pages 193-211
An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models....Pages 212-226
Context-Bounded Translations for Concurrent Software: An Empirical Evaluation....Pages 227-244
One Stack to Run Them All....Pages 245-261
Back Matter....Pages -
