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

Advanced Methods for Automatic Verification of Infinite-state Systems

Pokročilé techniky automatické verifikace nekonečně stavových systémů

grant

formal verification, infinite-state systems, model checking

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.).

Vojnar Tomáš, prof. Ing., Ph.D. (DITS) – research leader
Bouajjani Ahmed
Češka Milan, prof. RNDr., CSc.
Habermehl Peter
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Smrčka Aleš, Ing., Ph.D. (DITS)
Touili Tayssir, Dr., Ph.D.