Short implementation examples of abstract interpretation

Question

I am taking a course on abstract interpretation, but I haven't seen any examples of how the theory maps down to actual code.

I am looking for short code examples, where I preferably won't have to work with a whole compiler. The analysis doesn't have to be useful, I would just like to see an example where the analysis is derived and then implemented.

Does anyone know of any such examples, perhaps from a university course?

Answer 1

There is this paper by Bertot

Structural abstract interpretation, A formal study using Coq

That gives a full implementation of an abstract interpreter for a simple toy language using the Coq Proof Assistant. I used this for a concrete reference, and found it useful, although a little hard going, which is to be expected given the subject matter. Coq is a great little piece of software.

I also came across in a Cousot paper:

A gentle introduction to formal verification of computer systems by abstract interpretation

rough details (but I am sure there will be useful citations for full details) of an implementation in Astrée, I am not familiar with Astrée, so didn't actually read that section, but I think it meets your criteria.

If you come across anymore, please let me know! Would especially like to see a prolog abstract interpreter.

Answer 2

Maybe this tool is also interesting for you: Interproc Analyzer

It is an abstract analyzer for a very simple language, which however offers interprocedural analyses. You can try out the analysis and get numerical invariants about the analyzed program. The source code is available (OCaml).

A really thorough and precise course, given by one of the "creators" of Abstract Interpretation, Patrick Cousot (already mentioned in one of the answers): MIT course about Abstract Interpretation. The course also offers assignments, in OCaml.

Answer 3

AI is based on a mathematic theory name Galois Connection. The theory is very simple:

1. Abstract the behaviour of the program.
2. Perform the analysis on the abstract level.

Galois connection: To relate the Actual and Abstract program.

This is the best tutorial I have seen so far about Abstract Interpretation:

Answer 4

There is MonoREIL, which comes with the recently open sourced tool BinNavi.

See here is a short intro.

Note that the context of the MonoREIL framework is not compilers but the analysis of binary code. Yet, it has been used for real world applications, see slide 34 ff of this introduction (which contains more formal background).