Online Proceedings from SPIN 2008
the 15th International SPIN Workshop on Model Checking Software

Invited Presentations

• Matthew Dwyer, Nebraska, Residual Checking of Safety Properties: prove what you can and monitor the leftovers
• Daniel Jackson, MIT, Patterns of Software Modelling: From Classic To Funky
• Shaz Qadeer, Microsoft, Context-bounded verification of concurrent software
• Wolfram Schulte, Microsoft, Using dynamic symbolic execution to improve deductive verification
• Yannis Smaragdakis, Oregon, Combining Static and Dynamic Reasoning for the Discovery of Program Properties

Full Papers

• Todd Andel and Alec Yasinsac. Automated Evaluation of Secure Route Discovery in MANET Protocols (pdf)
• Harald Fecher and Sharon Shoham. State focusing: Lazy abstraction for the mu-calculus (pdf)
• Stefan Leue, Alin Stefanescu and Wei Wei. Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes (pdf)
• Radu Mateescu and Emilie Oudot. Improved On-the-Fly Equivalence Checking using Boolean Equation Systems (pdf)
• Sami Evangelista. Dynamic Delayed Duplicate Detection for External Memory Model Checking (pdf)
• Moonzoo Kim, Yunja Choi, Yunho Kim and Hotae Kim. Formal Verification of a Flash Memory Device Driver - an Experience Report (pdf)
• Dejvuth Suwimonteerabuth, Javier Esparza and Stefan Schwoon. Symbolic Context-Bounded Analysis of Multithreaded Java Programs (pdf)
• Frank Ciesinski, Christel Baier, Marcus Groesser and David Parker. Translating ProbMela specifications into the PRISM language (pdf)
• Malay Ganai and Aarti Gupta. Efficient Modeling of Concurrent Systems in BMC (pdf)
• Peter Lamborn and Eric Hansen. Layered Duplicate Detection in External-Memory Model Checking (pdf)
• Abed Nazha, Stavros Tripakis and Jean-Marc Vincent. System verification using randomized exploration of a large state space (pdf)
• Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan and Robert M. Kirby. Efficient Stateful Dynamic Partial Order Reduction (pdf)
• Gaurav Singh and Sandeep Shukla. Verifying Compiler Based Refinement of Bluespec Specifications using the SPIN Model Checker (pdf)
• Fang Yu, Tevfik Bultan, Marco Cova and Oscar Ibarra. Symbolic String Verification: An Automata-based Approach (pdf)
• Anna Zaks and Rajeev Joshi. Verifying Multi-threaded C Programs with SPIN (pdf)
• Viet Yen Nguyen and Theo Ruys. Incremental Hashing for Spin (pdf)
• Tonglaga bao and Michael Jones. Model Checking Abstract Components within Concrete Software Environments (pdf)

Tool Paper

• Gerard Holzmann, Rajeev Joshi and Alex Groce. Tackling large verification problems with the Swarm tool (pdf)