Abstract interpretation

Abstract interpretation is a mathematical framework for sound program analysis that replaces concrete program states with simpler abstract states. It uses sound approximations to infer properties such as possible values, reachability, and errors.

Concrete semantics: A mathematical account of a program's behavior in its concrete states and values. It defines the behavior that abstract domains approximate.
Operational semantics: A formal description of computation in terms of transitions between program configurations. Its transitions provide a concrete account of program execution to be approximated.
Static program analysis: Analysis of program properties without executing the program on ordinary inputs. Abstract interpretation supplies a general mathematical foundation for many static analyses.
Patrick Cousot: A French computer scientist known for foundational work on abstract interpretation and static analysis. He co-developed the framework and its mathematical foundations.
Abstract domain: A structured set of simplified program properties ordered by how much information they express. It represents the properties an analysis can compute instead of enumerating concrete states.
Lattice (order theory): A partially ordered set in which every pair of elements has a least upper bound and greatest lower bound. Lattice structure organizes abstract facts by precision and supports joins at control-flow merges.
Interval analysis: A numerical analysis that approximates each variable's possible values by an interval. Intervals form a simple abstract domain for proving bounds and detecting some arithmetic errors.
Radhia Cousot: A computer scientist known for foundational work on abstract interpretation and static program analysis. She co-developed the framework and established its early theory.
Galois connection: A pair of monotone maps between ordered sets that relates abstraction to concretization. It formalizes how abstract descriptions correspond to sets of concrete states.
Monotone function: A function between ordered sets that preserves their ordering. Monotone transfer functions make iterative analysis equations amenable to fixpoint reasoning.

Linked from 9 pages