P. Cousot, A Lagrangian relaxation and mathematical programming framework for static analysis and verification

Patrick Cousot.
A Lagrangian relaxation and mathematical programming framework for static analysis and verification.
LOPSTR'04 and SAS'04 invited talk, Verona, Italy. August 28, 2004.
Abstract:
     Program analysis involves an abstraction of the program semantics leading to inequations for fixpoint approximation that can be solved by iteration-based or constraint-based methods. Constraint-based static analysis and verification is the main subject of this talk.
     We briefly recall reachability and inevitability program properties and the iterated forward/backward iteration-based approximate static analysis which provides necessary (but in general insufficient) reachability and inevitability preconditons. The method is extended using backward decreasing counters which are shown to provide stronger necessary correctness preconditions.
     We then concentrate on the analysis and verification of sufficient conditions for the verification of inevitability properties of while loops performing linear, quadratic, ... and more generally semialgebraic numerical computations.
     To prove inevitability properties by Floyd's invariance and rank function methods, one must solve constraints (given by Floyd's verification conditions) which involve the discovery of a function on states (invariant or ranking function), and the proof of verification conditions involving an implication (e.g. between the pre and post conditions) and a universal quantification (over the values of the program variables).
     We first fix the form of the function on states in a parameterized form, which is an abstraction. It remains to determine the unkown parameters which involves implication and quantifier elimination.
     We show how the problem can be solved thanks to Tarski-Seidenberg-Collins quantifier elimination (implemented in Mathematica^®) with a worst-case time-complexity for real quantifier elimination which is “only” doubly exponential in the number of quantifier blocks but is unusable in practice, even on small programs. So we turn to numerical methods.
     We first show how to eliminate the implication by Lagrangian relaxation and discuss the particular linear case (affine Farkas' lemma) and quadratic case (Yakubovitch S-procedure).
     After a brief survey of mathematical programming, we then show that, in case the operational semantics of the 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.
     We present several examples, mainly loop termination proofs, and discuss the necessary tuning of semidefinite programming solvers under Matlab^® to avoid problems with feasibility.
     We then introduce conditional Lagrangian relaxation to handle disjunctions in loop tests and conditionals in loop bodies. We then consider nested loops and nondeterminacy (for concurrency and fair termination).
     Finally we consider the case of semialgebraic programs for which quantifiers can be eliminated by semidefinite programming relaxation by expressing the positivity of polynomials as an equality with a sum of squares.
     In conclusion we discuss data structures (use of norms), the impact of numerical errors and related work (for the linear case).
Slides of the 60mn presentation: .pdf

Bibliography:

\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,
}

copyright notice.
Last modified: Monday, 07-May-2012 17:51:05 EDT