Publication Details
Bounded Model Checking Using Java PathFinder
Model Checking, Java PathFinder, Bounded model checking, verification, Record&Replay trace, self-healing, concurrency, healing assurance
This work describes the using of bounded model checking for verification of the true races in programs.
This work describes the using of bounded model checking for verification of the true races in programs. The model checking of a real system is costly, thus there are some modification or alternations of model checking of features. This paper describes the search strategy for replaying a trace and for navigating through a state space to a suspicious state and a subsequent bounded model checking initiated from this state. The bounded model checking is implemented by the model checker Java Pathfinder.
@INPROCEEDINGS{FITPUB8718,
author = "Vendula Dudka",
title = "Bounded Model Checking Using Java PathFinder",
pages = "247--249",
booktitle = "Proceedings of the 14th Conference STUDENT EEICT 2008",
series = "Volume 2",
year = 2008,
location = "Brno, CZ",
publisher = "Brno University of Technology",
ISBN = "978-80-214-3615-2",
language = "english",
url = "https://www.fit.vut.cz/research/publication/8718"
}