Abstract Interpretation of Annotated Commands
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.
pdf
BibTeX:
@inproceedings{Nipkow-ITP12,
author={Tobias Nipkow},
title={Abstract Interpretation of Annotated Commands},
booktitle={Interactive Theorem Proving (ITP 2012)},
editor={Beringer and Felty},
publisher=Springer,series=LNCS,volume={7406},pages={116-132},year=2012}