Skip to content

Abstracts.2019.AI

Jump to bottom
Nachi Vpn edited this page Feb 3, 2020 · 5 revisions

Abstract Interpretation

by Matthías Páll Gissuarson

Abstract

In this talk, I will present Abstract Interpretation, an idea from program analysis, first described by Cousot & Cousot in 1977. It is based on three main ideas:

  1. Any static analysis/reasoning refers to a semantics describing, at some level of abstraction, its possible executions.

  2. The static analysis should abstract all semantic properties irrelevant to the reasoning.

  3. Undecidability entails that any sound, fully automated, and always terminating reasoning of a computer system must perform mathematical inductions in the abstract and can thus only be an approximate.

Abstract Interpretation formalizes the idea of "abstraction" and "approximation" using lattices, how they are connected by adjoints that "abstract" and "concretize", and the guarantees we can extract from those.

Clone this wiki locally