Editing Abstract interpretation (section)

== Abstract interpretation of computer programs ==

Given a programming or specification language, abstract interpretation consists of giving several semantics linked by relations of abstraction. A semantics is a mathematical characterization of a possible behavior of the program. The most precise semantics, describing very closely the actual execution of the program, are called the ''concrete semantics''. For instance, the concrete semantics of an [[imperative programming]] language may associate to each program the set of execution traces it may produce &ndash; an execution trace being a sequence of possible consecutive states of the execution of the program; a state typically consists of the value of the program counter and the memory locations (globals, stack and heap). More abstract semantics are then derived; for instance, one may consider only the set of reachable states in the executions (which amounts to considering the last states in finite traces).

The goal of static analysis is to derive a computable semantic interpretation  at some point. For instance, one may choose to represent the state of a program manipulating integer variables by forgetting the actual values of the variables and only keeping their signs (+, − or 0). For some elementary operations, such as [[multiplication]], such an abstraction does not lose any precision: to get the sign of a product, it is sufficient to know the sign of the operands. For some other operations, the abstraction may lose precision: for instance, it is impossible to know the sign of a sum whose operands are respectively positive and negative.

Sometimes a loss of precision is necessary to make the semantics decidable (see [[Rice's theorem]] and the [[halting problem]]). In general, there is a compromise to be made between the precision of the analysis and its decidability ([[computability theory (computation)|computability]]), or tractability ([[computational complexity|computational cost]]).

In practice the abstractions that are defined are tailored to both the program properties one desires to analyze, and to the set of target programs. The first large scale automated analysis of computer programs with abstract interpretation was motivated by the accident that resulted in the destruction of the [[Ariane 5 Flight 501|first flight of the Ariane 5]] rocket in 1996.<ref>{{cite web|title=PolySpace Technologies History | last=Faure | first=Christèle | url=http://christele.faure.pagesperso-orange.fr/polyspace.html | access-date=3 October 2010}}</ref>