Abstract:
We will introduce basic algorithms for static analysis
of programs by Abstract Interpretation in infinite abstract
domains using widening and narrowing.
We will then discuss the soundness and (in)completeness of
static analyzers with respect to formal properties of
program executions formalized by an operational semantics.
This yields to the notion of hierarchy of Abstract Interpretations
of a semantics, with applications to various forms of descriptions
of the semantics of grammars or programming languages, model-checking,
deductive methods, types, static analysis, etc. all viewed as
abstract semantics.
We will finish by an explanation of abstract mathematical induction,
which allows us to understand at a very high level of abstractions
recent static analysis methods, such as Graig interpolants.
\bibitem{PCousot-TASE-tutorial-15}
P.~Cousot.
\newblock A Gentle Tutorial on Abstract Interpretation.
\newblock In \emph{9th International Symposium on Theoretical Aspects of Software Engineering},
Nanjing, China, 12-14 September 2015.