Program Analysis

Catalog description

This course covers both foundations and practical aspects of the automated analysis of programs, which is becoming increasingly critical to find software errors and assure program correctness. The theory of abstract interpretation captures the essence of a broad range of program analyses and supports reasoning about their correctness. Building on this foundation, the course will describe program representations, data flow analysis, alias analysis, interprocedural analysis, dynamic analysis, Hoare Logic and verification, program synthesis and repair, model checking, and symbolic execution. Through assignments and projects, students will design and implement practical analysis tools that find bugs and verify properties of software. This course satisfies the Logic and Languages constrained elective category of the Computer Science major, the Theoretical Foundations requirement of the Computer Science master's degree, and the Technical Software Engineering requirement for the Software Engineering minor. Prerequisites: 15-251 Min. grade C and ( 17-214 or 15-150 Min. grade C) Course Website: https://cmu-program-analysis.github.io/