Is there any (general) formalization of abstract interpretation?

I am specifically looking for something as general as possible, i.e. not just a specific example of abstract interpretation, but a general proof of the concept based on lattice assumptions.
Does anyone have any pointers for me?

If you read french, you can have a look to the PhD thesis of David Pichardie https://davidpichardie.github.io/papers/these-pichardie.pdf (otherwise, maybe this paper: https://davidpichardie.github.io/papers/fics08.pdf )

1 Like

These might be relevant:

1 Like

I suppose the second link is the code to the paper in the first. But what about the third reference? Can you provide any context to it? Is there a paper or some explanation of it?

If you are interested in an elementary didactic presentation of abstract interpretation for a toy programming language, I addressed this topic in lecture notes visible here:

The material for these lecture notes is included in

It is maintained and probably compatible with coq-8.15, but you can ping me if you encounter any problem.

The Verasco static analyzer is not quite “general proof of the concept”, but rather a specific implementation, but its implementation covered various problems that can occur in practice when using abstract interpretation for implementing a static analyzer.

I don’t think that a generic formalization is of great help when you actually formalize a static analyzer, because actual static analyzer have a tendency to “not fill the mould” of the theoretic abstract interpretation, because of technical details, even though such static analyzers actually take a lot of inspiration from the theory of abstract interpretation.

For more information, you can have a look at the website, the POPL paper and my PhD thesis.

1 Like

I think that code eventually ended up serving as a companion for http://alsibahi.xyz/assets/pps/HankinFestschrift-2020-paper.pdf