Directed Model Checking with Distance-Preserving Abstractions

Dräge, Klaus; Finkbeiner, Bernd; Podelski, Andreas; Valmari, Antti

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Directed Model Checking with Distance-Preserving Abstractions

MPS-Authors

/persons/resource/persons45201

Podelski, Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Dräge, K., Finkbeiner, B., & Podelski, A. (2006). Directed Model Checking with Distance-Preserving Abstractions. In Model checking software : 13th International SPIN Workshop (pp. 19-34). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-228F-D

Abstract

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.