Formal Verification, Theory, Techniques and Tools

Model-Checking, Abstract-Interpretation

The work on formal verification includes model-checking techniques, and abstract-Interpretation techniques. Lesar is a symbolic or enumerative model-checker for Lustre. NBac is an abstract interpretation tool developed by B. Jeannet during his PhD in the group. Recent work on abstract interpretation techniques includes the verification of the properties of imperative algorithms that depend on the contents of arrays, and general theory for abstract interpretation.

 Abstract Interpretation

Program analysis by abstract interpretation is a long-standing research topic in the team, aiming at complementing model-checking techniques with analyses able to take into account numerical properties and data structures. During the considered period, these works took place first within the APRON, and now within the new project ASOPT (static analysis and optimisation) of the ANR programme Arpege (2009-11). In 2007, the arrival of David Monniaux, moving from Patrick Cousot’s team at ENS, was of course a very positive event for this theme.

David Merchat’s thesis was devoted to Cartesian factoring of polyhedra in linear relation analysis (LRA). The results were published in FMSD [1].


Verification of Array properties

Such analysis is faced with the problem of aliasing : changing a cell A[i] may silently change A[j], if it happens that i = j. As a consequence, we first proposed an analysis deciding whether, at a given program point, two variables are alway different. This was the subject of Mathias Péron’s master thesis [2] and was published in VMCAI’07 [3].

Then, we considered the automatic discovery of properties involving array contents, and we proposed an analysis for simple programs (handling one-dimensional arrays by simple iteration), which is able, for instance, to discover that the result of an insertion sort procedure is indeed a sorted array. This was published in PLDI’08 [4]. Moreover, we defined an analysis for discovering that an array is a permutation of another array (which, continuing the previous example, terminates the proof of the sorting procedure : not only the result is sorted, but it is a permutation of the initial array).


Exact abstract fixpoint computation and modular analysis

Two well-known weaknesses of most approaches of static program analysis by abstract interpretation are the computation of fixed points using widen- ings (the classical way of enforcing termination in abstract interpretation) and the lack of modularity.

Concerning widening, it is sometimes possible to compute least fixed points or good approximations thereof directly. In the case of LRA (linear relation analysis) we identified many cases of program loops the abstract effect of which can be computed exactly without iterations : in these cases, the analysis is both more precise and more efficient. Moreover, this technique is compatible with the use of widening, and therefore does not restrict the applicability of the analysis. This work took place in the thesis of Laure Gonnord, and was published in SAS’06 [5].

Another approach is to reduce the fixed point problem to a quantifier elimination problem (see POPL’09 paper [6]).

Not only is it possible to exactly solve the least fixed point problem for certain classes of programs and domains, this approach is also modular in the sense that the abstract transfer function of a sub-program can be compiled once and for all. Unfortunately the state of the art in quantifier elimination is not yet satisfactory for this method to scale up well. This led us to work on improvements to quantifier elimination algorithms (see LPAR’08 paper [7]) based on modern SMT-solving techniques. Another promising direction is to use numerical algorithms from operational research, but these, implemented in floating-point, usually do not provide assurance that their results are correct. We therefore researched how certain floating-point algorithms can be safely applied to accelerate some exact constraint computations (see CAV’09 paper [8]).

[1N. Halbwachs, D. Merchat, and L. Gonnord. Some ways to reduce the space dimension in polyhedra computations. Formal Methods in System Design, 29(1):79-­95, 2006.

[2M. Péron. IS, un domaine numérique abstrait pour l’analyse de programmes manipulant des adresses. Master thesis, Université Joseph Fourier, June 2005

[3M. Péron and N. Halbwachs. An abstract domain extending difference-bound matrices with disequality constraints. In B. Cook and A. Podelski, editors, 8th International Conference on Verification, Model- checking, and Abstract Intepretation, VMCAI’07, Nice, France, 2007.

[4N. Halbwachs and M. Péron. Discovering properties about arrays in simple programs. In ACM Conference on Programming Language Design and Implementation, PLDI 2008, pages 339-­348, Tucson (Az.), 6 2008

[5L. Gonnord and N. Halbwachs. Combining widening and acceleration in linear relation analysis. In 13th International Static Analysis Symposium, SAS’06, Seoul, Korea, 2006

[6David Monniaux. Automatic modular abstractions for linear constraints. In POPL (Principles of programming languages). ACM, 2009

[7David Monniaux. A quantifier elimination algorithm for linear real arithmetic. In LPAR (Logic for Programming Artificial Intelligence and Reasoning), volume 5330 of Lecture Notes in Computer Science, pages 243-­257. Springer Verlag, 2008

[8David Monniaux. On using floating-point computations to help an exact linear arithmetic decision procedure. In Computer-aided verification (CAV), volume 5643 of Lecture Notes in Computer Science, pages 570-­583. Springer Verlag, 2009


Contact | Plan du site | Site réalisé avec SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4193735