# jonny goes to england

London & co

## Abstract Interpretation

(source ilachinski.com)

I realized I don’t write a lot about what I’m actually doing day in day out for work. This is partly because it is thought as “hard to describe” to non-computer science people. Today, I want to describe a method which is widely used in the software verification community in an easy way.

The technique is called Abstract Interpretation (AI from now on) and has been first described by Cousot in 1976/77 [1]. Now, to describe AI I’ll directly start with an example also partly taken from [1]:

Imagine you are presented with the following calculation $3948 * 729 * 98573$.

Now I’m asking you to tell me the result of this multiplication without the help of a calculator. Obviously, unless you are a scary person, you don’t know the result because it is too complex to calculate in your head. However, when I change the question and ask you to tell me the sign of the result of this multiplication you will tell me instantly that the result is positive. How did you know that? Most probably you used your old highschool knowledge that the multiplication of positive numbers yields a positive result. So you used, without actually realising it, an abstraction of the multiplication operator to get the correct answer. This is a kind of abstract interpretation.

What we learned so far is: Abstract interpretation is replacing the actual domain of the answer (in our case the set of integers) with an abstract domain, in our case the sign domain which has only two elements $\{pos,\ neg\}$. Also, it is replacing the normal operations with abstract operations. Our abstract multiplication operation $\otimes$ has the following properties on the sign domain:

$pos \otimes pos = pos$

$pos \otimes neg = neg, neg \otimes pos = neg$

$neg \otimes neg = pos$

Now all that is missing is an abstraction function from the concrete domain to the abstract domain. This is defined as follows

$\alpha(n) = pos, \text{if } n \in \mathbb Z^{+} \cup \{0\}$

$\alpha(n) = neg, \text{if } n \in \mathbb Z^{-}$

Using these definitions we can easily solve the problem from above:

$\alpha(3948) \otimes (\alpha(729) \otimes \alpha(98573)) = pos \otimes (pos \otimes pos) = pos$

Now you could define more abstract operators on the sign domain and you would end up with a full abstract interpreter for basic mathematical operations. Cool, isn’t it?

To sum up, this technique is simplifying a problem by abstracting away information you don’t need to solve the problem (e.g. only getting the sign of a computation). The nice thing then is that the more abstract version is easier to calculate and the abstract result is saying something about the concrete result!

Of course, the sign domain is very primitive and has only limited use. Real abstract interpreter support many different abstract domains but the idea is always the same.

—-

[1] Cousot, P. and Cousot, R. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los Angeles, California, January 17 – 19, 1977). POPL ’77. ACM, New York, NY, 238-252. DOI= http://doi.acm.org/10.1145/512950.512973

http://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml

Written by jk

December 30, 2007 at 2:15 pm

Posted in english, technical

### 2 Responses

1. Wow, the paper is from 1977.

Daniel Lorch

December 30, 2007 at 8:17 pm

2. This was a very, very good post. Now I grokked what you really are up to! Please keep updating as time goes by.

The idea is very beautiful, almost mythological in the core: one does abstractions and more abstractions in the level of ideas, then creates a rule to collapse the whole structure to the concrete world – to make it “real”, one utters the words which do the linking from the divine realm of angels, infinity and brightness to the domain of humans, limitedness and dirt. (Yeah I guess I’ve read too much Joseph Campbell lately… 🙂