<p>There is this paper by Bertot</p>

<p><a href="http://arxiv.org/abs/0810.2179" rel="nofollow">Structural abstract interpretation, A formal study using Coq</a> </p>

<p>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.</p>

<p>I also came across in a Cousot paper:</p>

<p><a href="http://www.di.ens.fr/~cousot/COUSOTpapers/MARKTOBERDORF-09.shtml" rel="nofollow">A gentle introduction to formal verification of computer systems by abstract interpretation</a></p>

<p>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. </p>

<p>If you come across anymore, please let me know! Would especially like to see a prolog abstract interpreter.</p>
Short implementation examples of abstract interpretation
<p>I am taking a course on abstract interpretation, but I haven't seen any examples of how the theory maps down to actual code.</p>

<p>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.</p>

<p>Does anyone know of any such examples, perhaps from a university course?</p>