β Scribed by Matthew B. Dwyer, Rahul Purandare (auth.), Klaus Havelund, Rupak Majumdar, Jens Palsberg (eds.)
No coin nor oath required. For personal study only.
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.
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 -
Software Engineering; Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs
π SIMILAR VOLUMES
<P>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.</P><P>The 15 revised full papers presented were carefully reviewed and selected from 45 submissions; in addition there are 4 too
<p>The SPIN workshop is a forum for researchers interested in the subject of automata-based, explicit-state model checking technologies for the analysis and veri?cation of asynchronous concurrent and distributed systems. The SPIN - del checker (http://netlib.bell-labs.com/netlib/spin/whatispin.html)
<p><P>This book constitutes the refereed proceedings of the 10th International SPIN workshop on Model Checking of Software, SPIN 2003, held in Portland, OR, USA in May 2003 as an ICSE 2003 satellite workshop.</P><P>The 14 revised full papers and 3 revised tool papers presented were carefully reviewe
<p>Since 1995, when the SPIN workshop series was instigated, SPIN workshops have been held on an annual basis in MontrΒ΄ eal (1995), New Brunswick (1996), Enschede (1997), Paris (1998), Trento (1999), Toulouse (1999), Stanford (2000), Toronto (2001), Grenoble (2002) and Portland (2003). All but the ?