Trail-directed model checking

Citations of this article
Mendeley users who have this article in their library.


HSF-SPIN is a Promela model checker based on heuristic search strategies. It utilizes heuristic estimates in order to direct the search for finding software bugs in concurrent systems. As a consequence, HSF-SPIN is able to find shorter trails than blind depth-first search. This paper contributes an extension to the paradigm of directed model checking to shorten already established unacceptable long error trails. This approach has been implemented in HSF-SPIN. For selected benchmark and industrial communication protocols experimental evidence is given that trail-directed model-checking effectively shortcuts existing witness paths. © 2001 Published by Elsevier Science B.V.




Edelkamp, S., Lluch-Lafuente, A., & Leue, S. (2001). Trail-directed model checking. In Electronic Notes in Theoretical Computer Science (Vol. 55, pp. 343–356).

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free