> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/600-toc/620-formal-language-theory/abstract-interpretation.md).

# Abstract interpretation

<https://en.wikipedia.org/wiki/Abstract_interpretation>

*Abstract interpretation* is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a *partial execution* of a computer program which gains information about its semantics (e.g. data and control flow) without performing all the calculations.

Its main concrete application is *formal static analysis*, the automatic extraction of information about the possible executions of computer programs. Such analyses have two main usages:

* inside compilers, to analyse programs to decide whether certain optimizations or transformations are applicable
* for debugging or even the certification of programs against classes of bugs.
