The proof of correctness of programs being undecidable, automatic program verifiers must approximate these fixpoint constraints by abstract interpretation of the program semantics. The abstract equations must then be solved either iteratively or directly (e.g. by elimination).

     The seminar is devoted to the direct resolution of these constraints for sequential, nondeterministic, concurrent and fair parallel polynomial programs by a new method based on Lagrangian relaxation to handle implication and mathematical programming to handle quantifiers. It 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 and nonconvex optimization.

\bibitem{Cousot-Cambridge_18_10_2004}
P{.} Cousot.
\newblock Automatic program verification by Lagrangian relaxation and 
          semidefinite programming.
\newblock Semantics lunch, Theory and Semantics Group, The Computer
          Laboratory, University of Cambridge, Cambridge, UK. 18
          October 2004.

@conference{Cousot-Cambridge_18_10_2004,
   author =    {P{.} Cousot},
   title =     {Automatic program verification by Lagrangian relaxation and 
                semidefinite programming},
   booktitle = {Semantics lunch},
   address =   {Theory and Semantics Group, The Computer Laboratory, 
                University of Cambridge, Cambridge, UK},
   month =     {18 October},
   year =      2004,
}