Tree Automata In Modelling And Verification Of Concurrent Programs

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Tree Automata In Modelling And Verification Of Concurrent Programs

Original language description

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

Czech name

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

Czech description

Článek zkoumá možnosti modelování a verifikace paralelních programů s neomezenou rekurzí a neomezenou tvorbou vláken pomocí regulárního model checkingu zobecněného na práci se stromovými automaty.

Type

D - Article in proceedings

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

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

Publication year

2004

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Proceedings of ASIS 2004

ISBN

80-86840-03-4

ISSN

—

e-ISSN

—

Number of pages

6

Pages from-to

197-202

Publisher name

NEUVEDEN

Place of publication

Ostrava

Event location

Sv. Hostýn

Event date

Sep 22, 2004

Type of event by nationality

EUR - Evropská akce

UT code for WoS article

—