Trail-Directed Model Checking

Stefan Edelkamp, Alberto Lluch Lafuente, Stefan Leue

Research output: Contribution to journalConference articleResearchpeer-review


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.
Original languageEnglish
JournalTheoretical Computer Science
Issue number3
Pages (from-to)343-356
Publication statusPublished - 2001
Externally publishedYes
Event1st Workshop on Software Model Checking - , Denmark
Duration: 1 Oct 2001 → …
Conference number: 1


Conference1st Workshop on Software Model Checking
Period01/10/2001 → …


Dive into the research topics of 'Trail-Directed Model Checking'. Together they form a unique fingerprint.

Cite this