Stromové automaty v modelování a verifikaci paralelních programů

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F04%3APU49269" target="_blank" >RIV/00216305:26230/04:PU49269 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Tree Automata In Modelling And Verification Of Concurrent Programs

Popis výsledku v původním jazyce

We consider the problem of automated formal verification of modern concurrent software systems. Dealing with such systems, which involves handling unbounded dynamic instantiation, recursion, etc., naturally leads to a need of dealing with infinite statespaces. We suppose states of such systems to be viewed as terms with a tree structure and in the future, we would like to use the regular tree model checking method for dealing with infinite sets of states. Infinite sets of states are to be finitely desccribed by tree automata and their transformations by tree transducers. To facilitate the termination of the method, we intend to use a generalization of the abstract regular model checking method proposed for linear words. In the paper, we discuss the starting points of our work, the problems to be solved, and briefly sketch our first preliminary steps in the area---namely steps leading to a library for handling tree automata and transducers to be used as a basis for our future verificati

Název v anglickém jazyce

Tree Automata In Modelling And Verification Of Concurrent Programs

Popis výsledku anglicky

We consider the problem of automated formal verification of modern concurrent software systems. Dealing with such systems, which involves handling unbounded dynamic instantiation, recursion, etc., naturally leads to a need of dealing with infinite statespaces. We suppose states of such systems to be viewed as terms with a tree structure and in the future, we would like to use the regular tree model checking method for dealing with infinite sets of states. Infinite sets of states are to be finitely desccribed by tree automata and their transformations by tree transducers. To facilitate the termination of the method, we intend to use a generalization of the abstract regular model checking method proposed for linear words. In the paper, we discuss the starting points of our work, the problems to be solved, and briefly sketch our first preliminary steps in the area---namely steps leading to a library for handling tree automata and transducers to be used as a basis for our future verificati

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í

2004

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 ASIS 2004

ISBN

80-86840-03-4

ISSN

—

e-ISSN

—

Počet stran výsledku

6

Strana od-do

197-202

Název nakladatele

NEUVEDEN

Místo vydání

Ostrava

Místo konání akce

Sv. Hostýn

Datum konání akce

22. 9. 2004

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

EUR - Evropská akce

Kód UT WoS článku

—