Automates et Logique pour la vérification symbolique de logiciels

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.