Publication detail

Cut-offs and Automata in Formal Verification of Infinite-State Systems

VOJNAR, T.

Original Title

Cut-offs and Automata in Formal Verification of Infinite-State Systems

English Title

Cut-offs and Automata in Formal Verification of Infinite-State Systems

Type

book

Language

en

Original Abstract

In this work, we discuss two complementary approaches to formal verification of infinite-state systems---namely, the use cut-offs and automata-based symbolic model checking (especially the so-called regular model checking). The thesis is based on extended versions of multiple conference and journal papers joint into a unified framework and accompanied with a significantly extended overview of other existing approaches. The presented original results include cut-offs for verification of parameterised networks of processes with shared resources, the approach of abstract regular model checking combining regular model checking with the counterexample-guided abstraction refinement (CEGAR) loop, a proposal of using language inference for regular model checking, techniques for an application of regular model checking to verification of programs manipulating dynamic linked data structures, the approach of abstract regular tree model checking as well as a proposal of a novel class of tree automata with size constraints with applications in verification of programs manipulating balanced tree structures.

English abstract

In this work, we discuss two complementary approaches to formal verification of infinite-state systems---namely, the use cut-offs and automata-based symbolic model checking (especially the so-called regular model checking). The thesis is based on extended versions of multiple conference and journal papers joint into a unified framework and accompanied with a significantly extended overview of other existing approaches. The presented original results include cut-offs for verification of parameterised networks of processes with shared resources, the approach of abstract regular model checking combining regular model checking with the counterexample-guided abstraction refinement (CEGAR) loop, a proposal of using language inference for regular model checking, techniques for an application of regular model checking to verification of programs manipulating dynamic linked data structures, the approach of abstract regular tree model checking as well as a proposal of a novel class of tree automata with size constraints with applications in verification of programs manipulating balanced tree structures.

Keywords

Formal verification, infinite-state systems, model checking, cut-offs, symbolic model checking, regular model checking.

RIV year

2007

Released

21.12.2007

Publisher

Faculty of Information Technology BUT

Location

Brno

ISBN

978-80-214-3547-6

Edition

FIT Monograph 1

Pages count

189

Documents

BibTex


@book{BUT61919,
  author="Tomáš {Vojnar}",
  title="Cut-offs and Automata in Formal Verification of Infinite-State Systems",
  annote="In this work, we discuss two complementary approaches to formal verification of
infinite-state systems---namely, the use cut-offs and automata-based symbolic
model checking (especially the so-called regular model checking). The thesis is
based on extended versions of multiple conference and journal papers joint into a
unified framework and accompanied with a significantly extended overview of other
existing approaches.

The presented original results include cut-offs for verification of parameterised
networks of processes with shared resources, the approach of abstract regular
model checking combining regular model checking with the counterexample-guided
abstraction refinement (CEGAR) loop, a proposal of using language inference for
regular model checking, techniques for an application of regular model checking
to verification of programs manipulating dynamic linked data structures, the
approach of abstract regular tree model checking as well as a proposal of a novel
class of tree automata with size constraints with applications in verification of
programs manipulating balanced tree structures.",
  address="Faculty of Information Technology BUT",
  chapter="61919",
  edition="FIT Monograph 1",
  howpublished="print",
  institution="Faculty of Information Technology BUT",
  year="2007",
  month="december",
  pages="0--0",
  publisher="Faculty of Information Technology BUT",
  type="book"
}