Replay Tracer & BMC

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

Result language
angličtina
Original language name
Replay Tracer & BMC
Original language description
This tool is about the using of bounded model checking for verification of the bugs in concurrent programs. There is the search strategy for navigation through a state space to a suspicious state (or to its surroundings) and a subsequent bounded model checking initialled from this state. In the first step is record the trace of running program. The second step is replay this trace in some model checker and verify a chosen place in state space only. One of the advantage of these strategy is that the model checking can be started from any of recorded states which precede the suspicious state. We are concentrate to program written in Java. The model checker for Java program has been chosen Java PathFinder JPF. There is record trace of the running of the program by the IBM ConTest
Czech name
—
Czech description
—

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

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

Internal product ID
RecRev
Technical parameters
Poskytováno pod Freeware licencí VUT v Brně (https://wis.fit.vutbr.cz/FIT/db/dir.php/dr/VZ2007/externiInformace/softwareNaWebu/Priloha2_rozh23.pdf). - Implementovaný v programovacím jazyce Java. - Modul model checkeru JPF, kte
Economical parameters
—
Owner IČO
00216305
Owner name
Vysoké učení technické v Brně

Similar results(10)