Welcome to the Program Analysis and Verification homepage
This course teaches techniques for statically approximating the dynamic behaviors of programs (that is, without running them). These techniques are used for a variety of purposes such as compiler optimizations, bug finding (or rather proving the absence of bugs), program understanding, refactoring, etc. The mathematical foundation of the learned techniques will be the theory of abstract interpretation.The course will combine both theory and practice of programming analysis, including theoretical assignments and programming assignments.
By the end of the course, you will gain skills for developing static analyses for challenging problems, be able to explain the theory behind those analyses, and be able to implement them for real code.
Teaching Aids and Materials
- The lectures are given using (Power Point) slides.
- The lectures are recorded.
- Some of the lectures include worksheets for practicing.
Grading
The course grade will be determined by:- 3-4 theoretical assignments and programming assignments: 50%
- Home exam: 50%
To obtain a passing grade for the course, you must obtain a passing grade (>56 for undergraduate students and >65 for graduate students) for each assignment.
Books
- Semantics with Applications: A Formal Introduction. Flemming Nielsen , Hanne Riis Nielsen, and Chris Hankin. Wiley Professional Computing, (240 pages, ISBN 0 471 92980 8), Wiley, 1992.
Available at the library and as an online version. - The Formal Semantics of Programming Languages: An Introduction. Glynn Winskel. Foundations of Computing. The MIT Press, 1993. ISBN: 9780262731034
- Principles of Program Analysis. Hanne Riis Nielsen and Flemming Nielsen.
Springer (Corrected 2nd printing, 452 pages, ISBN 3-540-65410-0), 2005.
Available at the library.