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.
Lectures
- Monday 10:30-12:30, Taub 8
News
Lecture Slides
02 Operational Semantics [pptx][pdf]
05 CSSV and pointer analyses [pptx][pdf]
06 Inter-procedural 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
Resources
- some software horror stories
- more software disasters
- introduction to abstract interpretation, and more in POPL79, here, and more informally here
- Abstract interpretation: a semantics-based tool for program analysis by Jones and Nielson.
- A gentle introduction to formal verification of computer systems by abstract interpretation
- Principles of Program Analysis (book)
- practical success stories: ASTREE SLAM
- cool related projects: TVLA SLAyer Terminator SAFE
- industry: AbsInt Coverity GrammaTech Parasoft Klocwork