Abstract Interpretation of Annotated Commands

Tobias Nipkow

This paper formalises 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 paper is simplicity of the formalisation, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics.


author={Tobias Nipkow},
title={Abstract Interpretation of Annotated Commands},
booktitle={Interactive Theorem Proving (ITP 2012)},
editor={Beringer and Felty},