Faculty of Information Technology, BUT

Publication Details

Tree Automata In Modelling And Verification Of Concurrent Programs

ROGALEWICZ Adam and VOJNAR Tomáš. Tree Automata In Modelling And Verification Of Concurrent Programs. In: Proceedings of ASIS 2004. Ostrava, 2004, pp. 197-202. ISBN 80-86840-03-4.
Czech title
Stromové automaty v modelování a verifikaci paralelních programů
Type
conference paper
Language
english
Authors
Keywords
formal verification, regular model checking, automated abstraction
Abstract
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 state spaces. 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 described 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 verification tool.
Published
2004
Pages
197-202
Proceedings
Proceedings of ASIS 2004
Conference
ASIS2004 - 26th International Autumn Colloquium - Advanced Simulation of Systems, Sv. Hostýn, CZ
ISBN
80-86840-03-4
Place
Ostrava, CZ
BibTeX
@INPROCEEDINGS{FITPUB7617,
   author = "Adam Rogalewicz and Tom\'{a}\v{s} Vojnar",
   title = "Tree Automata In Modelling And Verification Of Concurrent Programs",
   pages = "197--202",
   booktitle = "Proceedings of ASIS 2004",
   year = 2004,
   location = "Ostrava, CZ",
   ISBN = "80-86840-03-4",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7617"
}
Back to top