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

Patrick Cousot.
Program Termination Proofs by Parametric Abstraction and Semi-definite Programming.
Specialised Talk, Seminar Series, Department of Computing and Information Sciences, Kansas State University, Manhattan, Kansas, USA, September 6th, 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: 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.
Recording of the seminar:
- .wav

Bibliographic reference:

\bibitem{Cousot-CIS-Kstate-06-09-06}
P.~Cousot.
\newblock Program Termination Proofs by Parametric Abstraction, Lagrangian Relaxation
          Semi-Definite Programming.
\newblock \emph{Specialised Talk, Seminar Series, Department of Computing and Information 
          Sciences, Kansas State University}, Manhattan, Kansas, USA, September 6th, 2006.

@unpublished{Cousot-CIS-Kstate-06-09-06,
   author = {Patrick Cousot},
   title =  {Program Termination Proofs by Parametric Abstraction, Lagrangian Relaxation
            and Semi-Definite Programming},
   note =   {\emph{Specialised Talk, Seminar Series, Department of Computing and Information 
            Sciences, Kansas State University}, Manhattan, Kansas, USA},
   month = {6 September},
   year =      2006,
}

copyright notice
Last modified: Monday, 04-Jan-2010 13:51:05 CET