Bounded Model Checking Using Java PathFinder

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F08%3APU80196" target="_blank" >RIV/00216305:26230/08:PU80196 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Bounded Model Checking Using Java PathFinder
Original language description
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.
Czech name
Bounded model checking v nástroji Java PathFinder
Czech description
Článek se zabývá bounded model checkingem pro verifikaci programů se soubězností. <br>

Project
<a href="/en/project/GA102%2F07%2F0322" target="_blank" >GA102/07/0322: Advanced Formal Approaches in the Design and Verification of Computer-Based Systems</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2008
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Proceedings of the 14th Conference STUDENT EEICT 2008
ISBN
978-80-214-3615-2
ISSN
—
e-ISSN
—
Number of pages
3
Pages from-to
—
Publisher name
Brno University of Technology
Place of publication
Brno
Event location
FEKT VUT v Brně
Event date
Apr 24, 2008
Type of event by nationality
CST - Celostátní akce
UT code for WoS article
—

Similar results(10)