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.


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.