Int J Softw Tools Technol Transfer (2004) 6: 257--259 / Digital Object Identifier (DOI) 10.1007/s10009-004-0168-3

this paper the authors extend their previous work on directed explicitstate model checking [8] by reconciling it with partialorder concepts, in particular partial-order reduction. This form of automated state space compaction is essential M. Dwyer, S. Leue: The algorithmics of software model checking 259 to the success of explicit-state model checking in analyzing concurrent software models, and hence it needs to be proven that this reduction method is compatible with the directed model checking approach. The authors also introduce heuristics based on Hamming distances between a given error trail and the current system state that help in reducing the length of precomputed counterexamples. The authors apply their approach to various examples of models of real-life concurrent software systems and have implemented their methods in a heuristic extension of SPIN, called HSF-SPI