Techniques avancées pour la vérification de systémes a nombre d'états infini

One of the currently most studied approaches to formal verification is model
checking, which is attractive by its high degree of automation and at the same
time a high degree of precision. Most of the research on model checking has
so-far concentrated on systems with possibly large, but finite state spaces.
However, many systems that one encounters in practice are infinite-state.
Infinity can arise due to dealing with various kinds of unbounded data structures
such as push-down stacks needed for dealing with recursive procedures, FIFO (and
other kinds) of communication channels or waiting queues, unrestricted counters
(or integer variables), dynamic linked data structures (such as lists or trees).
Yet another source of infinity is then dealing with various kinds of parameters
(such as the maximum value of some variable, the maximum length of a queue, or
the number of processes in a system). Consequently, techniques applying model
checking in the area of infinite-state systems have begun to appear as well.

Among the most successful approaches to infinite-state model checking that have
been proposed so-far, an important role is played by symbolic methods based on
using various formalisms (such as logics, automata, grammars, etc.) for a finite
representation of infinite sets of reachable states. Members of the project team
have significantly contributed to the research in this area by several
internationally recognised and cited results including original methods of
symbolic, automata-based model checking combined with automated abstraction (the
so-called abstract regular model checking---ARMC, methods based on automatic
inference (learning) of regular languages representing sets of reachable states
from their samples, and a series of methods for verifying programs manipulating
dynamic linked data structures (using ARMC, automated detection of repeated
memory patterns, or different types of extended automata with constraints).

The efficiency of the current methods of model checking of infinite-state systems
is, however, still far from a broad practical applicability, and the classes of
systems and their properties of interest on which these methods are applicable
are also restricted. Therefore, the goal of the project is to contribute to the
research on methods of model checking of infinite-state systems in order to
significantly lift their current restrictions both in terms of efficiency as well
as generality.

In particular, in order to contribute to an increased efficiency of the existing
symbolic model checking approaches for infinite-state systems, the project will,
e.g., consider development of symbolic model checking approaches based on
non-deterministic automata (avoiding the determinisation step that turns out to
be one of the most expensive steps in the current approaches). This implies
a need of development of all the needed automata operations (such as emptiness
checking, inclusion checking, minimisation, abstraction) for different kinds
non-deterministic automata (word automata, tree automata, etc.). In the area of
increasing the generality of the existing approaches, the project will consider
both dealing with more general systems (e.g., programs with unrestricted dynamic
linked data structures and integer variables) as well as dealing with more
complex properties to be checked (such as termination or liveness properties). In
order to do so, the project will examine various extensions of the current
automata and logics (e.g., combining various classes of automata and logics
describing in a qualitative way the structure of system configurations with
various numerical constraints) and also of the procedures of dealing with them
(including advanced decision procedures over logics, new abstraction and
inference methods over automata, etc.).