Model Checking Software

This volume contains the proceedings of the 15th International SPIN Workshop on Model Checking of Software (SPIN 2008), which took place at the University of California, Los Angeles, August 10-12, 2008. The SPIN workshops form a forum for researchers and practitioners interested in model checking techniques for the veri?cation and validation of software systems. Model checking is the process of checking whether a given structure is a model of a given logical f- mula.The structure normallyrepresents a setof tasks executing in parallelin an interleaved fashion, resulting in a non-deterministic set of executions. The main focusoftheworkshopseriesissoftwaresystems,including models andprograms. Subjects of interest include theoretical and algorithmic foundations as well as toolsfor softwaremodel checking.The workshopin additionaimsto foster int- actions and exchanges of ideas with related areas in software engineering, such as static analysis, dynamic analysis, and testing. There were 41 submissions, including 38 full papers and 3 tool papers. Each submissionwasreviewedbyatleastthreeProgrammeCommitteemembers.The committee decided to accept 18 papers, including 17 regular papers and 1 tool paper. The programme also included ?ve invited talks (in alphabetical order): Matthew Dwyer (University of Nebraska) "Residual Checking of Safety Pr- erties", Daniel Jackson (MIT) "Patterns of Software Modelling: From Classic To Funky", Shaz Qadeer (Microsoft Research) "The Case for Context-Bounded Veri?cation of Concurrent Programs", Wolfram Schulte (Microsoft Research) "Using Dynamic Symbolic Execution to Improve Deductive Veri?cation", and Yannis Smaragdakis (University of Oregon) "Combining Static and Dynamic Reasoning for the Discovery of Program Properties".