Static Analysis by Abstract Interpretation: A Mathematical Programming Approach

Static analysis of a computer program by abstract interpretation helps prove behavioural properties of the program. Programs are defined by means of a forward collecting semantics function relating the values of the program variables during the execution of the program. The least fixed point of the semantics function is a program invariants providing useful information about the program's behaviour. Mathematical Programming is a formal language for describing and solving optimization problems expressed in very general terms. This paper establishes a link between the two disciplines by providing a mathematical program that models the problem of finding the least fixed point of a semantics function. Although we limit the discussion to integer affine arithmetic semantics in the interval domain, the flexibility and power of mathematical programming tools have the potential for enriching static analysis considerably.