P. Cousot, Program Verification by Parametric Abstraction and Semi-definite Programming

Patrick Cousot.
Program Verification by Parametric Abstraction and Semi-definite Programming (invited talk).
Logic and Algorithms Workshop “Constraints and Verification”, Isaac Newton Institute for Mathematical Sciences, Cambridge, United Kingdom, 8—12 May 2006.
Abstract:
     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.
Keywords:
Program verification, invariance, termination, rank function, Lagrangian relaxation, semidefinite programming, linear matrix inequalities, bilinear matrix inequalities.
Slides of the 55 mn presentation: .pdf.

Recording of the seminar:
- .wav

Bibliographic reference:

\bibitem{Cousot-INI06}
P.~Cousot.
\newblock Program Verification by Parametric Abstraction and Semi-definite Programming (invited talk).
\newblock \emph{Logic and Algorithms Workshop ``Constraints and Verification''}, 
         Isaac Newton Institute for Mathematical Sciences, Cambridge, United Kingdom, 8--12 May 2006.

@inProceedings{Cousot-INI06,
   author =    {P{.} Cousot},
   title =     {Program Verification by Parametric Abstraction and Semi-definite Programming (invited talk)},
   booktitle = {Logic and Algorithms Workshop ``Constraints and Verification''},
   address =   {Isaac Newton Institute for Mathematical Sciences, Cambridge, United Kingdom},
   month =     {8--12 May},
   year =      2006,
}

copyright notice
Last modified: Monday, 07-May-2012 17:51:04 EDT