In this habilation thesis, we discuss two comlementary approchces 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 acompanied 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 counterexampleguided 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 applacations in verification of programs manipulating balanced tree strustures

Zpět na vědecké spisy