  


Code verification by static analysis: a mathematical programming approach
Jeremy Leconte (jeremylecontehotmail.com) 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 overapproximations $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 overflowtype 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 MixedInteger Linear Program for code based on integer arithmetic, and a MixedInteger Nonlinear Program otherwise. These programs can then be solved to guaranteed global optimality by means of general purpose BranchandBound 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 Modify/Update this entry  
Visitors  Authors  More about us  Links  
Subscribe, Unsubscribe Digest Archive Search, Browse the Repository

Submit Update Policies 
Coordinator's Board Classification Scheme Credits Give us feedback 
Optimization Journals, Sites, Societies  