Result Details

Tree Automata In Modelling And Verification Of Concurrent Programs

ROGALEWICZ, A.; VOJNAR, T. Tree Automata In Modelling And Verification Of Concurrent Programs. Proceedings of ASIS 2004. Ostrava: Marq software s.r.o., 2004. p. 197-202. ISBN: 80-86840-03-4.
Type
conference paper
Language
English
Authors
Abstract

We consider the problem of automated formal verification of modernconcurrent software systems. Dealing with such systems, which involveshandling unbounded dynamic instantiation, recursion, etc., naturallyleads to a need of dealing with infinite state spaces. We supposestates of such systems to be viewed as terms with a tree structure andin the future, we would like to use the regular tree model checkingmethod for dealing with infinite sets of states. Infinite sets ofstates are to be finitely described by tree automata and theirtransformations by tree transducers. To facilitate the termination ofthe method, we intend to use a generalization of the abstract regularmodel checking method proposed for linear words. In the paper, wediscuss the starting points of our work, the problems to be solved, andbriefly sketch our first preliminary steps in the area---namely stepsleading to a library for handling tree automata and transducers to beused as a basis for our future verification tool.

Keywords

formal verification, regular model checking, automated abstraction

Published
2004
Pages
197–202
Proceedings
Proceedings of ASIS 2004
Conference
ASIS2004 - 26th International Autumn Colloquium - Advanced Simulation of Systems
ISBN
80-86840-03-4
Publisher
Marq software s.r.o.
Place
Ostrava
BibTeX
@inproceedings{BUT17569,
  author="Adam {Rogalewicz} and Tomáš {Vojnar}",
  title="Tree Automata In Modelling And Verification Of Concurrent Programs",
  booktitle="Proceedings of ASIS 2004",
  year="2004",
  pages="197--202",
  publisher="Marq software s.r.o.",
  address="Ostrava",
  isbn="80-86840-03-4"
}
Projects
Advanced Methods of Automatic Verification of Parametric and Infinite-State Systems, GACR, Postdoktorandské granty, GP102/03/D211, start: 2003-09-01, end: 2006-09-01, completed
Automated methods and tools supporting development of reliable parallel and distributed systems, GACR, Standardní projekty, GA102/04/0780, start: 2004-01-01, end: 2006-12-31, completed
Research groups
Departments
Back to top