Publication Details

Bounded Model Checking Using Java PathFinder

DUDKA Vendula. Bounded Model Checking Using Java PathFinder. In: Proceedings of the 14th Conference STUDENT EEICT 2008. Volume 2. Brno: Brno University of Technology, 2008, pp. 247-249. ISBN 978-80-214-3615-2.
Czech title
Bounded model checking v nástroji Java PathFinder
Type
conference paper
Language
english
Authors
Dudka Vendula, Ing. (FIT BUT)
Keywords

Model Checking, Java PathFinder, Bounded model checking, verification, Record&Replay trace, self-healing, concurrency, healing assurance

Abstract

This work describes the using of bounded model checking for verification of the true races in programs.

Annotation

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.

Published
2008
Pages
247-249
Proceedings
Proceedings of the 14th Conference STUDENT EEICT 2008
Series
Volume 2
Conference
Student EEICT 2008, Brno, CZ
ISBN
978-80-214-3615-2
Publisher
Brno University of Technology
Place
Brno, CZ
BibTeX
@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"
}
Back to top