Main Page

From Averiss

The goal of this project is to provide advanced techniques for automatic software verification, taking into account complex features of software systems written in modern and widely used programming languages (e.g., C, Java, C++, etc). Among the important features to consider, we mention for instance : data manipulation, procedure calls, parameterization, process creation, concurrency, inclusion of external code, etc.

The approach we plan to develop in order to tackle the problem is based on a tight combination of (1) abstraction techniques, applicable directly to the source code of the programs, allowing to extract automatically accurate, potentially infinite-state, automata-based models, and (2) algorithmic techniques for the (exact/approximate) analysis of these expressive models. The applicable abstractions must be automatically defined, and refined by need using the result of the analysis. The analysis techniques will be based on symbolic model-checking for infinite-state systems using finite (automata/logic-based) representations of infinite sets of system configurations.

We intend developing algorithmic verification methods for both the verification of safety properties as well as for checking termination of programs. Moreover, these verification problems will be considered for closed systems (where all components are fully defined) as well as in the case of open systems where some of their components are partially specified (e.g., for the case of programs with external code invoking).

The verification methods and techniques developed in the project will be implemented in new software verification tools, and will be experimented on challenging verification problems of real size software systems such as kernels of operating systems and web servers.

read more...