Our objective in this talk is to give an intuitive account of abstract interpretation theory [
1][
2][
3][
4][
5] and to present and discuss its main applications [
6]. Abstract interpretation theory formalizes the conservative approximation of the semantics of hardware or software computer
systems. The
semantics provides a formal model describing all possible behaviors of a computer system in interaction with any possible environment.
By
approximation we mean the observation of the semantics at some level of abstraction, ignoring irrelevant details.
Conservative means that the approximation can never lead to an erroneous conclusion.
Abstract interpretation theory provides thinking tools since the idea of abstraction by conservative approximation is central to reasoning (in particular on computer systems) and
mechanical tools since the idea of an effectively computable approximation leads to a systematic and constructive formal design methodology
of automatic semantics-based program manipulation algorithms and tools (e.g. [7]).