Aim and Scope

In the first part of this course you will learn how to extract high-level information from (lower level) programs without running them. You will learn to statically (at compile time) reason about properties of programs. For example, how to use automatic program analysis techniques for showing that a web-site is not exposed to certain security vulnerabilities.

In the second part of the course, you will learn how to synthesize programs from (higher-level) partial programs and specifications.


  • Monday 10:30-12:30, Taub 8


Homework is available on here

Lecture Slides

01 Introduction  [pptx][pdf]

02 Operational Semantics  [pptx][pdf]

03 AI Basics  [pptx][pdf]

04 Numerical  [pptx][pdf]

05 CSSV and pointer analyses  [pptx][pdf]

06 Inter-procedural Analysis  [pptx][pdf]

07 Shape Analysis  [pptx][pdf]

08a Shape Analysis (Cont'd)  [pptx][pdf]

08b Typestate Verification  [pptx][pdf]

08c Predicate Abstraction  [pptx][pdf]

09 Abstraction-Guided Synthesis  [pptx][pdf]

10 Synthesis from Examples  [pptx][pdf]

11 Partial Programs, Program repair as a game, and sketeching  [pptx][pdf]



Course Requirements

  • homework assignments
  • lightweight project - you can choose between theoretical and practical
  • course notes