P. Cousot, Program termination proofs by convex optimization

Patrick Cousot.
Program termination proofs by convex optimization (invited talk).
IBM Programming Languages & Software Engineering Research Seminar, Thomas J.\ Watson Research Center, Hawthorne, NY, USA, 5 january 2007.
Abstract:
Program termination 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 termination conditions. For static program analysis, the discovery of the inductive arguments must be automated, which consists in solving the constraints provided by the termination 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 termination 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 sequential, nondeterministic, concurrent, and fair parallel imperative polynomial 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: The color transparencies are available as 1 slide per lanscape page for projection (1/1), 2 slides per portrait page for reading (2/1) and 4 slides per lanscape page for printing (4/1), in:
- PostScript: 1/1 .ps.gz, 2/1 .ps.gz, 4/1 .ps.gz for viewing with GhostScript and GhostView or (color) printing;
- PDF: 1/1 .pdf, 2/1 .pdf, 4/1 .pdf to be used with Acrobat Reader.

Bibliographic reference:

\bibitem{Cousot-INI06}
P.~Cousot.
\newblock Program termination proofs by convex optimization (invited talk).
\newblock \emph{IBM Programming Languages \& Software Engineering Research Seminar}, 
         Thomas J.\ Watson Research Center, Hawthorne, NY, USA, 5 january 2007.

@inProceedings{Cousot-INI06,
   author =    {P{.} Cousot},
   title =     {Program termination proofs by convex optimization (invited talk)},
   booktitle = {IBM Programming Languages \& Software Engineering Research Seminar},
   address =   {Thomas J.\ Watson Research Center, Hawthorne, NY, USA},
   month =     {7 January},
   year =      2006,
}

copyright notice
Last modified: Monday, 04-Jan-2010 13:48:32 CET