Abstract Interpretation of Annotated Commands

Tobias Nipkow 🌐

November 23, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This is the Isabelle formalization of the material decribed in the eponymous ITP 2012 paper. It develops a generic abstract interpreter for a while-language, including widening and narrowing. The collecting semantics and the abstract interpreter operate on annotated commands: the program is represented as a syntax tree with the semantic information directly embedded, without auxiliary labels. The aim of the formalization is simplicity, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics. A similar (but more polished) development is covered in the book Concrete Semantics.


BSD License


Related publications

Session Abs_Int_ITP2012