First we express the program semantics in polynomial form. Then the unknown rank function and invariants are abstracted in parametric form. The implication in the Floyd/Naur/Hoare verification conditions is handle by abstraction into numerical constraints by Lagrangian relaxation. The remaining universal quantification is handled by semidefinite programming relaxation. Finally the parameters are computed using 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 total correctness of sequential, nondeterministic, concurrent, and fair parallel imperative polynomial programs and can easily be extended to other safety and liveness properties.
\bibitem{Cousot05-VMCAI}
P.~Cousot.
\newblock Proving Program Invariance and Termination by Parametric
Abstraction, Lagrangian Relaxation and Semidefinite Programming.
\newblock In \emph{Sixth International Conference on Verification, Model
Checking and Abstract Interpretation (VMCAI'05)}, pages 1--24,
Paris, France, January 17-19, 2005. Lecture Notes in Computer
Science, volume 3385, Springer, Berlin.
@inproceedings{Cousot05-VMCAI,
author = {Cousot, P{.}},
title = {Proving Program Invariance and Termination by Parametric
Abstraction, Lagrangian Relaxation and Semidefinite
Programming},
pages = {1--24},
booktitle = {Sixth International Conference on Verification, Model
Checking and Abstract Interpretation (VMCAI'05)},
address = {Paris, France, LNCS 3385},
publisher = {Springer, Berlin},
month = jan # " 17--19",
year = 2005,
isbn = {978-3-540-24297-0},
issn = {0302-9743},
doi = {10.1007/b105073},
url = {http://www.springerlink.com/content/qkufe4uekjgyja4f/},
}