-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2019.AI
by Matthías Páll Gissuarson
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:
-
Any static analysis/reasoning refers to a semantics describing, at some level of abstraction, its possible executions.
-
The static analysis should abstract all semantic properties irrelevant to the reasoning.
-
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.
- Patrick Cousot & Radhia Cousot. "Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints." In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238—252, Los Angeles, California, 1977. ACM Press, New York, NY, USA.
A simple, intuitive, and informal introduction to abstract interpretation by Patrick Cousot is available from his web page: "Abstract Interpretation in a Nutshell."