Optimization Online


Code verification by static analysis: a mathematical programming approach

Jeremy Leconte (jeremyleconte***at***hotmail.com)
Stephane Le Roux (leroux***at***lix.polytechnique.fr)
Leo Liberti (liberti***at***lix.polytechnique.fr)
Fabrizio Marinelli (marinelli***at***diiga.univpm.it)

Abstract: Automatic verification of computer code is of paramount importance in embedded systems supplying essential services. One of the most important verification techniques is static code analysis by abstract interpretation: the concrete semantics of a programming language (i.e.the values $\chi$ that variable symbols {\tt x} appearing in a program can take during its execution) are replaced by abstract semantics (for example the assignment of convex over-approximations $X\supseteq\chi$ to {\tt x}). Using abstract semantics, we represent the effect of the program on $X$ by a function $F(X)$. All sets $X$ satisfying the condition $F(X)\subseteq X$ are such that all values outside $X$ are never assigned to {\tt x} during program execution. We are particularly interested in finding the {\it smallest} such $X$, which in itself satisfies the fixpoint equation $X=F(X)$: this allows (static) detection of several types of errors, such as overflow-type bugs. Traditionally, the equations $X=F(X)$ are solved computationally using Kleene's or Policy Iteration algorithms: these methods can only guarantee convergence to the smallest fixpoint $X$ under additional (often stringent) conditions. We propose a mathematical program whose constraints define the same space as $X\supseteq F(X)$ and whose objective function minimizes the size of $X$, whenever $X$ is an array of intervals. This yields a Mixed-Integer Linear Program for code based on integer arithmetic, and a Mixed-Integer Nonlinear Program otherwise. These programs can then be solved to guaranteed global optimality by means of general purpose Branch-and-Bound type algorithms.

Keywords: static analysis, abstract interpretation, kleene's iteration, debugging, MINLP, flowchart

Category 1: Applications -- Science and Engineering (Other )

Category 2: Integer Programming ((Mixed) Integer Nonlinear Programming )

Category 3: Optimization Software and Modeling Systems (Modeling Languages and Systems )

Citation: LIX, Ecole Polytechnique, Palaiseau, France; Aug. 2009

Download: [PDF]

Entry Submitted: 08/14/2009
Entry Accepted: 08/14/2009
Entry Last Modified: 09/26/2009

Modify/Update this entry

  Visitors Authors More about us Links
  Subscribe, Unsubscribe
Digest Archive
Search, Browse the Repository


Coordinator's Board
Classification Scheme
Give us feedback
Optimization Journals, Sites, Societies
Mathematical Programming Society