Článek ve sborníku konference

 
Hrubá, V.: Bounded Model Checking Using Java PathFinder, In: Proceedings of the 14th Conference STUDENT EEICT 2008, Brno, CZ, VUT v Brně, 2008, s. 247-249, ISBN 978-80-214-3615-2
Jazyk publikace:angličtina
Název publikace:Bounded Model Checking Using Java PathFinder
Název (cs):Bounded model checking v nástroji Java PathFinder
Strany:247-249
Sborník:Proceedings of the 14th Conference STUDENT EEICT 2008
Konference:Student EEICT 2008
Řada knih:Volume 2
Místo vydání:Brno, CZ
Rok:2008
ISBN:978-80-214-3615-2
Vydavatel:Vysoké učení technické v Brně
Klíčová slova
Model Checking, Java PathFinder, Bounded model checking, verifikace, Record&Replay trace, automatická oprava, souběžnost, ověřování opravy
Anotace
Článek se zabývá bounded model checkingem pro verifikaci programů se soubězností.
Abstrakt
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.
BibTeX:
@INPROCEEDINGS{
   author = {Vendula Hrubá},
   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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=8718}
}