Directed Model Checking (DMC) is an approach that proposes the use of AI-inspired heuristic search strategies in order to improve model checking techniques.

During my research in that area we implemented an experimental model checker called HSF-SPIN (, manual), which can be seen as an extension to the model checker Spin.

Since experimenting was crucial I also collected a lot of Promela specifications.

More details on DMC can be found in the following documents and the references therein:

  • Partial-Order Reduction for General State Exploring Algorithms
    Dragan Bosnacki, Stefan Leue, Alberto Lluch Lafuente, International Journal on Software Tools for Technology Transfer (STTT), Volume 11, Number 1, 2009.
    bib
  • Partial-order reduction and trail improvement in directed model checking
    Stefan Edelkamp, Stefan Leue, Alberto Lluch Lafuente, International Journal on Software Tools for Technology Transfer (STTT), Volume 6, Number 4, November 2004. bib
  • Directed explicit-state model checking in the validation of communication protocols
    Stefan Edelkamp, Stefan Leue, Alberto Lluch Lafuente, International Journal on Software Tools for Technology Transfer (STTT), Volume 5, Numbers 2-3, June 2003. bib
  • Heuristic Search for the Analysis of Graph Transition Systems
    Stefan Edelkamp, Shahid Jabbar, Alberto Lluch Lafuente, International Conference on Graph Transformation (ICGT) Natal, 2006.
    abstract bib
  • Abstraction Databases in Theory and Model Checking Practice
    Stefan Edelkamp, Alberto Lluch Lafuente, ICAPS Workshop on Connecting Planning Theory with Practice, June 2004.
    abstract bib
  • Symmetry Reduction and Heuristic Search for Error Detection in Model Checking
    Alberto Lluch Lafuente, Workshop on Model Checking and Artificial Intelligence, August 2003.
    abstract bib
  • Directed Search for the Verification of Communication Protocols
    Alberto Lluch Lafuente, PhD Thesis, Freiburger Dokument Server,  Institute of Computer Science, University of Freiburg, June 2003.
    abstract bib

See also the Dagstuhl and the ICAPS seminars and Stefan Edelkamp’s on the topic.