Patrick Cousot (ENS), Program Verification by Parametric Abstraction, Lagrangian Relaxation and Semi-Definite Programming

Program verification is based on reasonings by induction (e.g. on program steps, program data) which involves the discovery of unknown inductive arguments (e.g. rank functions, invariants) satisfying universally quantified verification conditions.

For static program analysis, the discovery of the inductive arguments must be automated, which consists in solving the constraints provided by the verification conditions. Several methods have been considered: recurrence/difference equation resolution; iteration, possibly with convergence acceleration through widening/narrowing; or direct methods (such as elimination). All these methods involve some form of simplification of the constraints formalized by abstract interpretation.

In this talk, we explore parametric abstraction of rank function and invariants and direct resolution of Floyd/Naur/Hoare verification constraints by Lagrangian relaxation (to handle implication) and semidefinite programming relaxation (to handle universal implication). Finally the parameters are computed using numerical semidefinite programming solvers. This new approach exploits the recent progress in the numerical resolution of linear or bilinear matrix inequalities by semidefinite programming using efficient polynomial primal/dual interior point methods generalizing those well-known in linear programming to convex optimization.

The framework is applied to invariance and termination proof of sequen- tial, nondeterministic, concurrent, and fair parallel imperative polyno- mial programs and can easily be extended to other safety and liveness properties.