Bounded model checking v nástroji Java PathFinder

Kód výsledku v 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>
Výsledek na webu
—
DOI - Digital Object Identifier
—

Jazyk výsledku
angličtina
Název v původním jazyce
Bounded Model Checking Using Java PathFinder
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Bounded Model Checking Using Java PathFinder
Popis výsledku anglicky
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.

Projekt
<a href="/cs/project/GA102%2F07%2F0322" target="_blank" >GA102/07/0322: Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění
2008
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Podobné výsledky(10)