Abstract Interpretations with Boogie

May 28, 2010 at 2:00 PM

Hi everyone,

In the code I saw code for abstract interpretations for boogie. How are they used? Is there a way to extend the framework and add my own code for latices?

Thanks, Thorsten

Jun 1, 2010 at 2:29 PM

My concrete question is whether it is possible to "plug-in" new latices for custom types? Like in a similar way as the proovers, where a custom dll can be loaded.

Jun 5, 2010 at 2:54 AM

The abstract-interpretation framework in Boogie was built with the intention of being extensible.  However, we haven't played much with it for some time (other than using the simple interval domain, which is on by default), so the code is a bit dusty.  You can go into the code and add your own lattices (perhaps easiest is to search the code by looking for uses of the command-line switch /infer).  What would be much nicer, however, would be if you'd revise the abstract-interpretation interface so that one could specify /infer:MyInferenceEngine.dll on the command-line and have Boogie call out to the so-indicated DLLs.  The /prover switch does something similar as it calls out to a particular theorem prover.