Automates et Logique pour la vérification symbolique de logiciels

Automata and Logic for Symbolic Verification of Software

Automaty a logiky v symbolické verifikaci software

grant

formal verification, infinite-state systems, symbolic representations, automata, logics

Among
techniques which can be used for verification of infinite-state
systems, one can find approaches based on cut-offs, automated
induction, or symbolic
verification,
which is probably the most frequent and which is also the subject of
the proposed project. Symbolic verification is based on encoding
infinite sets of states of the examined systems (possibly after some
abstraction) in a finite way using some suitable formalism. Probably
the most commonly used symbolic representations are those built on
logics
and automata.

The
scientific
goal
of the proposed project is to significantly advance the state of the
art in the area of symbolic
logic-based and automata-based verification methods for
infinite-state software,
namely to increase the scalability of these approaches and to broaden
the area of their applicability. To achieve this goal we plan to
further improve the various individual logic-based as well as
automata-based techniques, but also invest a significant amount
of research into approaches combining
advantages of both automata as well as logics. In the research, we
will in particular concentrate on verification of programs with
unbounded integers, (parametrised-size) arrays, and complex dynamic
linked data structures.

Rogalewicz Adam, doc. Mgr., Ph.D. (DITS) – research leader
Bozga Marius
Habermehl Peter
Konečný Filip, Ing., Ph.D.
Radu Iosif
Šimáček Jiří, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)