ABSTRACT INTERPRETATION

ABSTRACT INTERPRETATION

Abstract interpretation is a mathematical theory to define and prove the soundness of abstractions. This theory was invented by Patrick and Radhia Cousot in 1977, and it led to an incredible amount of scientific and industrial results during the last 40 years.
The main idea is to formalize a concrete world defining the runtime semantics of a programming language, and an abstract world defining a computable approximation of the concrete world. Each world is made by a domain (formalizing the states of the execution and of the static analysis) and a semantics (formalizing the runtime behavior and their approximation of the statements of a programming language). In addition, in some circumstances it is necessary to define an operator on the abstract domain to ensure the convergence of the analysis. The abstract world is sound if certain properties hold w.r.t. the concrete world. We refer the interest reader to the 2012 ETH course on static program analysis taught by Pietro Ferrara (currently working at Julia).
Abstract interpretation of a jam recipe
Before deepen into software, let’s give a look to the overall idea of abstract interpretation. And let’s take something that has nothing to do with software: a jam recipe! As you can read, this recipe distinguishes among 4 different types of fruits: blackberries, plums, raspberries and strawberries. Each fruit requires some tuning in the recipe: for instance, blackberries requires 50ml of waters, while plums need 150ml before boiling.
How could we abstract such recipe? For instance, we might approximate the 4 cases for the different fruits all together. Let’s consider the first step in the recipe:

Put the fruit into a preserving pan or large heavy-based saucepan. For blackberries, add 50ml of water and 1 and half tbsp of lemon juice; for plums (halved and stoned), use 150ml of water; for strawberries, add 3 tbsp of lemon juice (no water); and for raspberries, add nothing. Bring to the boil.

This is the semantics of the system we are abstracting considering only a generic fruit instead of the 4 specific cases. So a sound approximation of this semantics step might be as follows:

Put the fruit into a preserving pan or large heavy-based saucepan. Add between 0ml and 150ml of water, and between 0 and 3 tbsp of lemon juice. Bring to the boil.

Of course this is just one of the possible abstractions: you could have just said to add some water, lemon joice, and then boil, and this would have been still a sound (but less precise) abstraction!
Abstract interpretation of code
You are now ready to apply abstract interpretation to software! Consider the following snipped of code, where size is an input from the user:

int[] array = new int[size];
for(int i=0; i<array.length; i++)
array[i]=0;

Even on this very simple and minimal example, it is almost impossible to compute all possible executions, as this would mean to run this program on all possible values of size. So, what kind of abstractions we could apply?
A first and very simple one consists in tracking the sign of variables. Imagine that + represents that a variable is greater than or equal to zero. Our analysis would be able to infer that, inside the body of the for loop variable i is +. This happens because i is initialized to zero, and then it is incremented by one (that is, a positive value is added to +, resulting still in a + value).
Another kind of abstraction might track the numerical interval of the possible values of variables. With this abstraction, we would track that i is [0..0] after initialization, and then, while iterating the abstract semantics of the for loop we will obtain the following sequence of intervals: [0..1], [0..2], [0..3], … For this abstraction, we need an operator that enforces the convergence of the analysis. Intuitively, this operator, after few iterations of the abstract semantics on the for loop, could approximate the value of i with the interval [0..+inf], reaching a so-called fixpoint in the analysis.
Applications of abstract interpretation to industrial software
In addition to thousands of scientific publications (the most relevant ones can be found here), abstract interpretation was the basis of several industrial static analyzers. The first industrial success of abstract interpretation happened in 1996. The Ariane 5 flight 501 was launched on June, 4th 1996, and exploded after 37” (video). This happened because an overflow in the computation of the flight controller that triggered the auto-destruction mechanism. Polyspace, a tool based on abstract interpretation, discovered automatically the bug. Another successful industrial application is ASTREE. This analyzer, developed by the Cousots’ scientific team, proved the absence of runtime errors in the flight control software of Airbus A340 and A380.
Julia is the only Java industrial static analyzer based on the abstract interpretation theory. His scientific committee is made by some of the major experts in this field. Prof. Fausto Spoto (co-founder of Julia) has published more than 50 scientific papers in the best conferences and journals of the field. Pietro Ferrara (research scientist at Julia) has been a PhD student of Radhia Cousot, a postdoc at ETH Zurich, and a Research Staff Member at the IBM T.J. Watson Research Center in New York state. Prof. Roberto Giacobazzi is one of the most recognized researchers in abstract interpretation. He was among the very first to introduce abstract interpretation in Italy with his master thesis in 1988, and has been working with the équipe Cousot in École Polythechnique in Paris for several years.
Contact Us

We're not around right now. But you can send us an email and we'll get back to you, asap.

Start typing and press Enter to search