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

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

Habilitation thesis

In this habilitation thesis, we discuss two complementary approaches to formalverification of infinite-state systems---namely, the use cut-offs and automata-based symbolic model checking (especially the so-called regularmodel checking). The thesis is based on extended versions of multiple conferenceand journal papers joint into a unified framework and accompanied with asignificantly extended overview of other existing approaches.

The presented original results include cut-offs for verification of parameterisednetworks of processes with shared resources, the approach of abstract regularmodel checking combining regular model checking with the counterexample-guidedabstraction refinement (CEGAR) loop, a proposal of using language inference forregular model checking, techniques for an application of regular model checkingto verification of programs manipulating dynamic linked data structures, theapproach of abstract regular tree model checking as well as a proposal of a novelclass of tree automata with size constraints with applications in verification ofprograms manipulating balanced tree structures.

In this habilitation thesis, we discuss two complementary approaches to formalverification of infinite-state systems---namely, the use cut-offs and automata-based symbolic model checking (especially the so-called regularmodel checking). The thesis is based on extended versions of multiple conferenceand journal papers joint into a unified framework and accompanied with asignificantly extended overview of other existing approaches.

The presented original results include cut-offs for verification of parameterisednetworks of processes with shared resources, the approach of abstract regularmodel checking combining regular model checking with the counterexample-guidedabstraction refinement (CEGAR) loop, a proposal of using language inference forregular model checking, techniques for an application of regular model checkingto verification of programs manipulating dynamic linked data structures, theapproach of abstract regular tree model checking as well as a proposal of a novelclass of tree automata with size constraints with applications in verification ofprograms manipulating balanced tree structures.

VOJNAR, T.

12.11.2006

FIT VUT v Brně

150

https://www.fit.vut.cz/research/publication/10700/

habilitation