Directed Model Checking with Distance-preserving Abstractions
Klaus Dräger, Bernd Finkbeiner, and Andreas Podelski
In directed model checking, the traversal of the state space is guided by an estimate of the distance from the current state to the nearest error state. This paper presents a distance-preserving abstraction for concurrent systems that allows one to compute an interesting estimate of the error distance without hitting the state explosion problem. Our experiments show a dramatic reduction both in the number of states explored by the model checker and in the total runtime.
Software Tools for Technology Transfer 2008 (STTT 2008).
Extended Version of the SPIN 2006 paper.