Abstract Interpretation - Abstract Interpretation of Computer Programs

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 – 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, halting problem). In general, there is a compromise to be made between the precision of the analysis and its decidability (computability), or tractability (complexity).

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 can be attributed to an accident that resulted in the destruction of the first flight of the Ariane 5 rocket in 1996.

Read more about this topic:  Abstract Interpretation

Famous quotes containing the words abstract, computer and/or programs:

    What persuades men and women to mistake each other from time to time for gods or vermin is ideology. One can understand well enough how human beings may struggle and murder for good material reasons—reasons connected, for instance, with their physical survival. It is much harder to grasp how they may come to do so in the name of something as apparently abstract as ideas. Yet ideas are what men and women live by, and will occasionally die for.
    Terry Eagleton (b. 1943)

    The Buddha, the Godhead, resides quite as comfortably in the circuits of a digital computer or the gears of a cycle transmission as he does at the top of a mountain or in the petals of a flower.
    Robert M. Pirsig (b. 1928)

    Although good early childhood programs can benefit all children, they are not a quick fix for all of society’s ills—from crime in the streets to adolescent pregnancy, from school failure to unemployment. We must emphasize that good quality early childhood programs can help change the social and educational outcomes for many children, but they are not a panacea; they cannot ameliorate the effects of all harmful social and psychological environments.
    Barbara Bowman (20th century)