jonny goes to england

Abstract Interpretation

Posted in english, technical by jonny on December 30th, 2007

abstract-new-15.jpg

(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(394 <img src='http://s.wordpress.com/wp-includes/images/smilies/icon_cool.gif' alt='8)' class='wp-smiley' /> \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

2 comments