Abstract interpretation and static analysis
|Presented by David Schmidt, Kansas State University http://www.cis.ksu.edu/~schmidt|
A static analysis finitely analyzes
a program in advance of the program's execution and
extracts information useful for program transformation
or program-correctness proofs.
Abstract interpretation is a foundational framework that
can justify the correctness of
a static analysis.
Many elegant static analyses are synthesized from the abstract
interpretations that justify their correctness.
This series of lectures introduces abstract interpretation and applies it to static analysis. Standard formats of static analysis are presented, and abstract interpretations are used to synthesize both abstract-operational- and abstract-denotational-semantics definitions and as well as logics and models for temporal-logic model checking.
References for further reading are attached to the end of each lecture.
Exam for Course
(Answer any three of the four questions on the exam.)