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.
Citation
LIX, Ecole Polytechnique, Palaiseau, France; Aug. 2009