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 (showing slides, my scribbles on the slides, and audio).
  • Some of the lectures include worksheets for practicing.


The course grade will be determined by:
  • Theoretical assignments and programming assignments: 50%
  • Exam: 50%

To obtain a passing grade for the course, you must obtain a passing grade (>56) for each assignment and for the exam.


  • 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.

  • 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.