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.