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, Room TBA
Course Requirements
- homework assignments
- lightweight project - you can choose between theoretical and practical
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