### 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.

### License

BSD License

### Topics

- Computer science/Programming languages/Static analysis

### Related publications

- Nipkow, T. (2012). Abstract Interpretation of Annotated Commands. Lecture Notes in Computer Science, 116–132. https://doi.org/10.1007/978-3-642-32347-8_9

### Session Abs_Int_ITP2012

- Complete_Lattice_ix
- ACom
- Collecting
- Abs_Int0
- Abs_State
- Abs_Int1
- Abs_Int2
- Abs_Int2_ivl
- Abs_Int3
- Abs_Int1_const
- Abs_Int1_parity

## Cite

×

Abs_Int_ITP2012-AFP

    @article{Abs_Int_ITP2012-AFP,
      author  = {Tobias Nipkow},
      title   = {Abstract Interpretation of Annotated Commands},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Abs_Int_ITP2012.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1