Cesta k použití Mony pro abstract regular tree model checking

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F05%3APU56410" target="_blank" >RIV/00216305:26230/05:PU56410 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Towards Applying Mona in Abstract Regular Tree Model Checking

Popis výsledku v původním jazyce

We consider the problem of automated formal verification of<br> modern concurrent software systems. Dealing with such systems, which involves<br> handling unbounded dynamic instantiation, recursion, etc., naturally leads to a<br> need of dealing with infinite state spaces. We suppose states of such systems<br> to be encoded terms with a tree structure and we would like to<br> use the abstract regular tree model checking method for dealing with infinite sets of states.<br> This paper presents an ongoingresearch on application of abstract regular model checking in<br> the infinite state systems verification, and possibility to use the Mona GTA library for experiments.<br> <br>

Název v anglickém jazyce

Towards Applying Mona in Abstract Regular Tree Model Checking

Popis výsledku anglicky

We consider the problem of automated formal verification of<br> modern concurrent software systems. Dealing with such systems, which involves<br> handling unbounded dynamic instantiation, recursion, etc., naturally leads to a<br> need of dealing with infinite state spaces. We suppose states of such systems<br> to be encoded terms with a tree structure and we would like to<br> use the abstract regular tree model checking method for dealing with infinite sets of states.<br> This paper presents an ongoingresearch on application of abstract regular model checking in<br> the infinite state systems verification, and possibility to use the Mona GTA library for experiments.<br> <br>

Druh

D - Stať ve sborníku

CEP obor

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

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2005

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 11th Conference Student EEICT 2005

ISBN

80-214-2890-2

ISSN

—

e-ISSN

—

Počet stran výsledku

5

Strana od-do

663-667

Název nakladatele

Faculty of Information Technology BUT

Místo vydání

Brno

Místo konání akce

Brno

Datum konání akce

28. 4. 2005

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

CST - Celostátní akce

Kód UT WoS článku

—