Directed model checking algorithms focus computation resources in the error-prone areas of concurrent systems. The algorithms depend on some empirical analysis to report their performance gains. Recent work characterizes the hardness of models used in the analysis as an estimated number of paths in the model that contain an error. This hardness metric is computed using a stateless random walk. We show that this is not a good hardness metric because models labeled hard with a stateless random walk metric have easily discoverable errors with a stateful randomized search. We present an analysis which shows that a hardness metric based on a stateful randomized search is a better baseline for hardness in models used to benchmark model checking techniques. Furthermore, we convert easy models into hard models as measured by our new metric by pushing the errors deeper in the system and manipulating the number of threads that actually manifest an error.

Pdf version

Conference Slides

N. Rungta and E. G. Mercer. “Hardness for Explicit State Software Model Checking Benchmarks,” 5th IEEE International Conference on Software Engineering and Formal Methods, London, U.K, September 2007.

@inproceedings{rungta:sefm07,
author = {N. Rungta and E. G. Mercer},
title = {Hardness for Explicit State Software Model Checking Benchmarks},
booktitle = {SEFM '07: Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods},
year = {2007},
isbn = {0-7695-2884-8},
pages = {247--256},
doi = {http://dx.doi.org/10.1109/SEFM.2007.23},
publisher = {IEEE Computer Society},
address = {Washington, DC, USA},
}