Publication detail

Tree Automata In Modelling And Verification Of Concurrent Programs

ROGALEWICZ, A., VOJNAR, T.

Original Title

Tree Automata In Modelling And Verification Of Concurrent Programs

English Title

Tree Automata In Modelling And Verification Of Concurrent Programs

Type

conference paper

Language

en

Original 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.

English 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.

Keywords

formal verification, regular model checking, automated abstraction

RIV year

2004

Released

22.09.2004

Location

Ostrava

ISBN

80-86840-03-4

Book

Proceedings of ASIS 2004

Pages from

197

Pages to

202

Pages count

6

Documents

BibTex


@inproceedings{BUT17569,
  author="Adam {Rogalewicz} and Tomáš {Vojnar}",
  title="Tree Automata In Modelling And Verification Of Concurrent Programs",
  annote="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.",
  booktitle="Proceedings of ASIS 2004",
  chapter="17569",
  year="2004",
  month="september",
  pages="197--202",
  type="conference paper"
}