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

The workshop was held in Los Angeles, USA, August 10-12, 2008. The final versions of all papers are published in Lecture Notes in Computer Science (LNCS) Vol. 5156, Springer-Verlag.

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)

Spin home page