# GetWiki

*Abstract interpretation*

ARTICLE SUBJECTS

being →

database →

ethics →

fiction →

history →

internet →

language →

linux →

logic →

method →

news →

policy →

purpose →

religion →

science →

software →

truth →

unix →

wiki →

ARTICLE TYPES

essay →

feed →

help →

system →

wiki →

ARTICLE ORIGINS

critical →

forked →

imported →

original →

Abstract interpretation

[ temporary import ]

**please note:**

- the content below is remote from Wikipedia

- it has been imported raw for GetWiki

**abstract interpretation**is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics (e.g., control-flow, data-flow) without performing all the calculations.Its main concrete application is formal static analysis, the automatic extraction of information about the possible executions of computer programs; such analyses have two main usages:

- inside compilers, to analyse programs to decide whether certain optimizations or transformations are applicable;
- for debugging or even the certification of programs against classes of bugs.

## Intuition

This section illustrates abstract interpretation by means of real-world, non-computing examples.Consider the people in a conference room. Assume a unique identifier for each person in the room, like a social security number in the United States. To prove that someone is not present, all one needs to do is see if their social security number is not on the list. Since two different people cannot have the same number, it is possible to prove or disprove the presence of a participant simply by looking up his or her number.However it is possible that only the names of attendees were registered. If the name of a person is not found in the list, we may safely conclude that that person was not present; but if it is, we cannot conclude definitely without further inquiries, due to the possibility of homonyms (for example, two people named John Smith). Note that this imprecise information will still be adequate for most purposes, because homonyms are rare in practice. However, in all rigor, we cannot say for sure that somebody was present in the room; all we can say is that he or she was*possibly*here. If the person we are looking up is a criminal, we will issue an

*alarm*; but there is of course the possibility of issuing a

*false alarm*. Similar phenomena will occur in the analysis of programs.If we are only interested in some specific information, say, "was there a person of age

*n*in the room?", keeping a list of all names and dates of births is unnecessary. We may safely and without loss of precision restrict ourselves to keeping a list of the participants' ages. If this is already too much to handle, we might keep only the age of the youngest,

*m*and oldest person,

*M*. If the question is about an age strictly lower than

*m*or strictly higher than

*M*, then we may safely respond that no such participant was present. Otherwise, we may only be able to say that we do not know.In the case of computing, concrete, precise information is in general not computable within finite time and memory (see Rice's theorem and the halting problem). Abstraction is used to allow for generalized answers to questions (for example, answering "maybe" to a yes/no question, meaning "yes or no", when we (an algorithm of abstract interpretation) cannot compute the precise answer with certainty); this simplifies the problems, making them amenable to automatic solutions. One crucial requirement is to add enough vagueness so as to make problems manageable while still retaining enough precision for answering the important questions (such as "may the program crash?").

## 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.WEB, PolySpace Technologies History, Faure, ChristÃ¨le,weblink 3 October 2010,

## Formalization

(File:Abstract interpretation of integers by signs svg.svg|thumb|Example: abstraction of integer sets (red) to sign sets (green))Let*L*be an ordered set, called a

**concrete set**and let

*L*′ be another ordered set, called an

**abstract set**. These two sets are related to each other by defining total functions that map elements from one to the other.A function Î± is called an

**abstraction function**if it maps an element

*x*in the concrete set

*L*to an element Î±(

*x*) in the abstract set

*L*′. That is, element Î±(

*x*) in

*L*′ is the

**abstraction**of

*x*in

*L*.A function Î³ is called a

**concretization function**if it maps an element

*x*′ in the abstract set

*L*′ to an element Î³(

*x*′) in the concrete set

*L*. That is, element Î³(

*x*′) in

*L*is a

**concretization**of

*x*′ in

*L*′.Let

*L*1,

*L*2,

*L*′1 and

*L*′2 be ordered sets. The concrete semantics

*f*is a monotonic function from

*L*1 to

*L*2. A function

*f*′ from

*L*′1 to

*L*′2 is said to be a

**valid abstraction**of

*f*if for all

*x*′ in

*L*′1, (

*f*âˆ˜ Î³)(

*x*′) â‰¤ (Î³ âˆ˜

*f*′)(

*x*′).Program semantics are generally described using fixed points in the presence of loops or recursive procedures. Let us suppose that

*L*is a complete lattice and let

*f*be a monotonic function from

*L*into

*L*. Then, any

*x*′ such that

*f*(

*x*′) â‰¤

*x*′ is an abstraction of the least fixed-point of

*f*, which exists, according to the Knaster–Tarski theorem.The difficulty is now to obtain such an

*x*′. If

*L*′ is of finite height, or at least verifies the ascending chain condition (all ascending sequences are ultimately stationary), then such an

*x*′ may be obtained as the stationary limit of the ascending sequence

*x*′

*n*defined by induction as follows:

*x*′0=âŠ¥ (the least element of

*L*′) and

*x*′

*n*+1=

*f*′(

*x*′

*n*).In other cases, it is still possible to obtain such an

*x*′ through a widening operator BOOK, P., Cousot, R., Cousot, Comparing the Galois Connection and Widening / Narrowing Approaches to Abstract Interpretation,weblink Maurice, Bruynooghe, Martin, Wirsing, Proc. 4th Int. Symp. on Programming Language Implementation and Logic Programming (PLILP), August 1992, 269â€“296, Springer, 978-0-387-55844-8, 631, Lecture Notes in Computer Science, âˆ‡: for all

*x*and

*y*,

*x*âˆ‡

*y*should be greater or equal than both

*x*and

*y*, and for any sequence

*y*′

*n*, the sequence defined by

*x*′0=âŠ¥ and

*x*′

*n*+1=

*x*′

*n*âˆ‡

*y*′

*n*is ultimately stationary. We can then take

*y*′

*n*=

*f*′(

*x*′

*n*).In some cases, it is possible to define abstractions using Galois connections (Î±, Î³) where Î± is from

*L*to

*L*′ and Î³ is from

*L*′ to

*L*. This supposes the existence of best abstractions, which is not necessarily the case. For instance, if we abstract sets of couples (

*x*,

*y*) of real numbers by enclosing convex polyhedra, there is no optimal abstraction to the disc defined by

*x*2+

*y*2 â‰¤ 1.

## Examples of abstract domains

One can assign to each variable*x*available at a given program point an interval [

*L*

**'x****,**

*H**'x*]. A state assigning the value

*v*(

*x*) to variable

*x*will be a concretization of these intervals if for all

*x*,

*v*(

*x*) is in [

*L*

**'x****,**

*H**'x*]. From the intervals [

*L*

**'x****,**

*H**'x*] and [

*L*

**'y****,**

*H**'y*] for variables

*x*and

*y*, one can easily obtain intervals for

*x*+

*y*([

*L*

**'x****+**

*L**'y*,

*H*

**'x****+**

*H**'y*]) and for

*x*âˆ’

*y*([

*L*

**'x****âˆ’**

*H**'y*,

*H*

**'x****âˆ’**

*L**'y*]); note that these are

*exact*abstractions, since the set of possible outcomes for, say,

*x*+

*y*, is precisely the interval ([

*L*

**'x****+**

*L**'y*,

*H*

**'x****+**

*H**'y*]). More complex formulas can be derived for multiplication, division, etc., yielding so-called interval arithmetics.BOOK, Patrick, Cousot, Radhia, Cousot, Static determination of dynamic properties of programs, Proceedings of the Second International Symposium on Programming, Dunod, Paris, France, 106â€“130, 1976,weblink Let us now consider the following very simple program:y = x;z = x - y;{| style="float:right"

thumb | interval arithmetic ({{color>#00ff00 | #00ffff | C (programming language)>C code ({{color | red}}: concrete sets of possible values at runtime). Using the congruence information ({{color | 0}}=even, {{color | 1}}=odd), a zero division can be excluded. (Since only one variable is involved, relational vs. non-relational domains is not an issue here.)]] |

**non-relational domain**. Non-relational domains tend to be fast and simple to implement, but imprecise.Some examples of

**relational**numerical abstract domains are:

- congruence relations on integersJOURNAL, Philippe, Granger, Static Analysis of Arithmetical Congruences, International Journal of Computer Mathematics, 30, 165â€“190, 1989, 10.1080/00207168908803778, BOOK, Philippe Granger, Static Analysis of Linear Congruence Equalities Among Variables of a Program, S., Abramsky, T.S.E., Maibaum, Proc. Int. J. Conf. on Theory and Practice of Software Development (TAPSOFT), Springer, Lecture Notes in Computer Science, 493, 169â€“192, 1991,
- convex polyhedraBOOK, Patrick, Cousot, Nicolas, Halbwachs, Automatic Discovery of Linear Restraints Among Variables of a Program, Conf. Rec. 5th ACM Symp. on Principles of Programming Languages (POPL), 84â€“97,weblink January 1978, (cf. left picture) â€“ with some high computational costs
- difference-bound matricesBOOK, Antoine, MinÃ©, A New Numerical Abstract Domain Based on Difference-Bound Matricesdate=2001

- "octagons"THESIS, Ph.D. thesis, Antoine, MinÃ©, Weakly Relational Numerical Abstract Domains, Laboratoire d'Informatique de l'Ã‰cole Normale SupÃ©rieure,weblink Dec 2004, JOURNAL, Antoine MinÃ©, The Octagon Abstract Domain, Higher Order Symbol. Comput., 19, 1, 31â€“100, 2006, 10.1007/s10990-006-8609-1, cs/0703084, JOURNAL, Robert, ClarisÃ³, Jordi, Cortadella, The Octahedron Abstract Domain, Science of Computer Programming, 64, 115â€“139,weblink 2007, 10.1016/j.scico.2006.03.009,
- linear equalitiesJOURNAL, Michael Karr, Affine Relationships Among Variables of a Program, Acta Informatica, 6, 133â€“151, 1976, 10.1007/BF00268497,

## Tools

### Sound tools

Sound tools guarantee that the verification they perform is correct and exhaustive. They can never yield false negatives, but by undecidability may produce false alarms (or false positive) signaling a potential error with no instance during any execution (because the static analysis is not precise enough to eliminate the potential error).- AbsInt Advanced AnalyzerCONFERENCE

, D.

, KÃ¤stner

, C.

, Ferdinand

, Efficient Verification of Non-Functional Safety Properties by Abstract Interpretation: Timing, Stack Consumption, and Absence of Runtime Errors

, Proceedings of the 29th International System Safety Conference ISSC2011 Las Vegas

,

,

, 2011

,

, AbsInt Advanced Analyzer

, KÃ¤stner

, C.

, Ferdinand

, Efficient Verification of Non-Functional Safety Properties by Abstract Interpretation: Timing, Stack Consumption, and Absence of Runtime Errors

, Proceedings of the 29th International System Safety Conference ISSC2011 Las Vegas

,

,

, 2011

,

, AbsInt Advanced Analyzer

- AstrÃ©e
- CodeContracts static checkerCodeContracts static checker (cccheck)
- CodePeer
- CPAchecker
- ECLAIR
- Fluctuat
- Frama-C value analysis
- IKOSIKOS
- Julia Static Analyzer for Java, Android and Java bytecodeJulia Static Analyzer for Java, Android and Java bytecode
- PenjiliPenjili
- Polyspace
- Predatorpredator
- VerascoVerasco

### Unsound tools

Unsound tools do not guarantee that the verification they perform is correct and exhaustive. They can yield false alarms/positive as well as false negative, not signaling an error that occur for at least one program execution, because the static analysis they perform is incorrect (i.e., they fail to consider some possible executions). As a consequence, they can falsely claim that an unsafe program is safe.- CodesonarCodesonar
- Coverity Prevent
- Klocwork Insight{{clarify|reason=The target article is about a static analysis tool in general, but is it not clear whether it employs abstract interpretation in particular. Establish a connection to the latter, or delete the link.|date=November 2013}}
- Parasoft C/C++test{{clarify|reason=The target article is about a static analysis tool in general, but is it not clear whether it employs abstract interpretation in particular. Establish a connection to the latter, or delete the link.|date=November 2013}}
- Parasoft Jtest{{clarify|reason=The target article is about a static analysis tool in general, but is it not clear whether it employs abstract interpretation in particular. Establish a connection to the latter, or delete the link.|date=November 2013}}
- Red Lizard's Goanna{{clarify|reason=The target article is about a static analysis tool in general, but is it not clear whether it employs abstract interpretation in particular. Establish a connection to the latter, or delete the link.|date=November 2013}}

## See also

- Standard interpretation
- Model checking
- Symbolic simulation
- Symbolic execution
- List of tools for static code analysis — contains both abstract-interpretation based (sound) and ad-hoc (unsound) tools
- Static program analysis — overview of analysis methods, including, but not restricted to, abstract interpretation

## References

{{Reflist|40em}}## External links

- A web-page on Abstract Interpretation maintained by Patrick Cousot
- Roberto Bagnara's paper showing how it is possible to implement an abstract-interpretation based static analyzer for a C-like programming language
- The Static Analysis Symposia, proceedings appearing in the Springer LNCS series
- Conference on Verification, Model-Checking, and Abstract Interpretation (VMCAI), affiliated at the POPL conference, proceedings appearing in the Springer LNCS series

- Lecture notes

- Abstract Interpretation. Patrick Cousot. MIT.
- David Schmidt's lecture notes on abstract interpretation
- MÃ¸ller and Schwarzbach's lecture notes on Static Program Analysis
- Agostino Cortesi's lecture notes on Program Analysis and Verification
- Slides by GrÃ©goire Sutre going through every step of Abstract Interpretation with many examples - also introducing Galois connections

**- content above as imported from Wikipedia**

- "

- time: 7:53pm EST - Sun, Nov 18 2018

- "

__Abstract interpretation__" does not exist on GetWiki (yet)- time: 7:53pm EST - Sun, Nov 18 2018

[ this remote article is provided by Wikipedia ]

LATEST EDITS [ see all ]

GETWIKI 09 MAY 2016

GETWIKI 18 OCT 2015

GETWIKI 20 AUG 2014

GETWIKI 19 AUG 2014

GETWIKI 18 AUG 2014

© 2018 M.R.M. PARROTT | ALL RIGHTS RESERVED