while
loops performing linear, quadratic, ...
and more generally semialgebraic numerical computations.
while
loop body can be expressed in Linear Matrix
Inequality (LMI) form, the universal quantifiers can be eliminated by
solving a feasibility problem with semidefinite programming
interior point methods thus providing values of the unkown parameters.
This covers linear and quadratic programs.
\bibitem{CousotSAS04} P{.} Cousot. \newblock A Lagrangian relaxation and mathematical programming framework for static analysis and verification. \newblock LOPSTR'04 and SAS'04 invited talk, Verona, Italy, 28 August 2004. @conference{CousotSAS04, author = {P{.} Cousot}, title = {A Lagrangian relaxation and mathematical programming framework for static analysis and verification}, booktitle = {LOPSTR'04 and SAS'04 invited talk, Verona, Italy}, month = {28 August}, year = 2004, }