Online Proceedings from SPIN 2007
14th International SPIN Workshop on Model Checking Software

The workshop was held in Berlin, Germany, July 1-3, 2007. The final versions of all papers are published in Lecture Notes in Computer Science (LNCS) Vol. 4595 by Springer-Verlag.

Invited Presentations

Directed Model Checking and SAT

  • Sharon Shoham and Harald Fecher, Univ. Kiel, Local abstraction-refinement for the mu-calculus (pdf)
  • Neha Rungta and Eric Mercer, Brigham Young Univ, Generating Counter-examples through Randomized Guided Search (pdf)
  • Paul Gastin, and Pierre Moro, CNRS and Univ. Paris, Minimal counter-example generation for SPIN (pdf)
  • Gerard Basler, Daniel Kroening, and Georg Weissenbacher, ETH Zurich, SAT-based Summarisation for Boolean Programs (pdf)

Partial Order Reduction

  • Sami Evangelista and Christophe Pajault, CEDRIC-CNAM Paris, Some Solutions to the Ignoring Problem (pdf)
  • Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, and Robert M. Kirby, Univ. Utah, Distributed Dynamic Partial Order Reduction based Verification of Threaded Software (pdf)
  • Guy Gueta, Mooly Sagiv, Eran Yahav, and Cormac Flanagan, Tel Aviv Univ, Univ. Santa Cruz, and IBM Watson, Cartesian Partial-Order Reduction (pdf)

Statespace Exploration

  • Kristin Y. Rozier and Moshe Y. Vardi, NASA Langley and Rice Univ., LTL Satisfiability Checking (pdf)
  • Michael Weber, CWI Amsterdam, An Embeddable Virtual Machine for State Space Generation (pdf)
  • Jiri Barnat, Petr Rockai, and Lubos Brim, Univ. Brno, Scalable Multi-Core LTL Model-Checking (pdf)

Modeling, Static Analysis, Case Studies

  • Joel Self and Eric Mercer, Brigham Young Univ, On-the-fly Dynamic Dead Variable Analysis (pdf)
  • Claus Traulsen, Florence Maraninchi, Matthieu Moy, and Jerome Cornet, Verimag and Univ Kiel, A SystemC/TLM semantics in Promela and its possible applications (pdf)
  • Alberto Lluch Lafuente, Univ. Pisa, Towards Model Checking Spatial Properties with SPIN (pdf)
  • Pedro de la Camara, Maria del Mar Gallardo, and Pedro Merino, Univ. Malaga, Model Extraction for ARINC 653 based Avionics Software (pdf)

Tool Presentations

  • Radek Pelanek, Univ. Brno, BEEM: Benchmarks for Explicit Model Checkers (pdf)
  • Maria del Mar Gallardo, Christophe Joubert, Pedro Merino Gomez, and David Sanan, Univ. Malaga and Univ. Valencia, C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs (pdf)
  • Mohamed Nassim Seghir and Andreas Podelski, Univ. Freiburg, ACSAR: Software Model Checking with Transfinite Refinement (pdf)
  • Swarat Chaudhuri and Rajeev Alur, Univ. of Penn., Instrumenting C programs with Nested Word Monitors (pdf)
Spin home page