"RecRev" . . "\u00A0\u00A0\u00A0- Implementovan\u00FD v programovac\u00EDm jazyce Java. \u00A0\u00A0\u00A0- Modul model checkeru JPF, kter\u00FD pomoc\u00ED listeneru a prohled\u00E1vac\u00ED strategie \u00A0\u00A0\u00A0\u00A0\u00A0umo\u017E\u0148uje navigaci stavov\u00FDm prostorem pomoc\u00ED zaznamenan\u00E9 cesty. \u00A0\u00A0\u00A0- Pro n\u011Bkter\u00E9 \u010D\u00E1sti je zapot\u0159eb\u00ED n\u00E1stroj IBM ConTest. \u00A0\u00A0\u00A0- Mo\u017Enost dal\u0161\u00EDho roz\u0161\u00ED\u0159en\u00ED o listenry a r\u016Fzn\u00E1 nastaven\u00ED prohled\u00E1v\u00E1n\u00ED \u00A0\u00A0\u00A0\u00A0\u00A0stavov\u00E9ho prostoru a nastaven\u00ED vlastn\u00EDho model checkeru. \u00A0\u00A0\u00A0\u00A0\u00A0Poskytov\u00E1no pod Freeware licenc\u00ED VUT v Brn\u011B \u00A0\u00A0\u00A0\u00A0\u00A0(https://wis.fit.vutbr.cz/FIT/db/dir.php/dr/VZ2007/externiInformace/softwar \u00A0\u00A0\u00A0\u00A0\u00A0eNaWebu/Priloha2_rozh23.pdf)." . . . . . "Vojnar, Tom\u00E1\u0161" . "Replay Tracer & BMC" . . . "K\u0159ena, Bohuslav" . "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" . "Replay Tracer & BMC"@en . "RIV/00216305:26230/10:PR25240" . . . . . "http://www.fit.vutbr.cz/research/groups/verifit/tools/RecRev" . "Replay Tracer & BMC" . . . . . . "[D53F601377D3]" . "284849" . "search strategy, model checking, bounded model checking, Java, verification"@en . "5"^^ . . "Letko, Zden\u011Bk" . . "RIV/00216305:26230/10:PR25240!RIV12-GA0-26230___" . . . "P(GAP103/10/0306), P(GD102/09/H042), P(OC10009), S, Z(MSM0021630528)" . "Hrub\u00E1, Vendula" . "http://www.fit.vutbr.cz/research/groups/verifit/tools/RecRev" . . "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"@en . "Replay Tracer & BMC"@en . . "26230" . "5"^^ . . "Fiedor, Jan" . . . . . . . "Software je voln\u011B dostupn\u00FD." .