Abstract Interpretation of Annotated Commands (Q7361337)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Abs_Int_ITP2012
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Abstract Interpretation of Annotated Commands |
AFP entry Abs_Int_ITP2012 |
Statements
23 November 2016
0 references
Tobias Nipkow
0 references
Abstract Interpretation of Annotated Commands (English)
0 references
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 .
0 references
