Bounded model checking v nástroji Java PathFinder

Kód výsledku v IS VaVaI

RIV/00216305:26230/08:PU80196 - isvavai.cz

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.

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

GA102/07/0322: Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů

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ů

Název statě ve sborníku

Proceedings of the 14th Conference STUDENT EEICT 2008

ISBN

978-80-214-3615-2

ISSN

—

e-ISSN

—

Počet stran výsledku

3

Strana od-do

—

Název nakladatele

Brno University of Technology

Místo vydání

Brno

Místo konání akce

FEKT VUT v Brně

Datum konání akce

24. 4. 2008

Typ akce podle státní příslušnosti

CST - Celostátní akce

Kód UT WoS článku

—