Abstract interpretation

Abstract interpretation is an approach to static program analysis formalized by Patrick Cousot and Radhia Cousot at the Laboratoire d’Informatique, Grenoble, France, in 1977. It enables the analysis of huge software projects by mapping concrete semantics to abstract semantics. Some precision is lost, but the abstraction only errs on the safe side.

Nowadays, abstract-interpretation–based tools are in wide industrial use and expressly recommended by safety standards such as DO-178C (aerospace), ISO-26262 (automotive) or prEN-50128 (railway).