Abstract Interpretation of Annotated Commands

Title:	Abstract Interpretation of Annotated Commands
Author:	Tobias Nipkow
Submission date:	2016-11-23
Abstract:	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.
BibTeX:	@article{Abs_Int_ITP2012-AFP, author = {Tobias Nipkow}, title = {Abstract Interpretation of Annotated Commands}, journal = {Archive of Formal Proofs}, month = nov, year = 2016, note = {\url{https://isa-afp.org/entries/Abs_Int_ITP2012.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.