CMSC631: Program Analysis and Understanding

Fall, 2020

The objective of this course is to introduce students to the complementary research areas of programming languages and program analysis. As such it covers basic theoretical ideas and practical techniques for modeling and analyzing programming languages; and leveraging those techniques to mechanically reason about programs. A significant portion of the course will be carried out using the Coq proof assistant, which permits students to program formal systems and automatically check that proofs about them are correct. The latter portion of the course will afford each student an opportunity to more deeply explore a relevant topic of their choice, as we will cover special topics at the forefront of PL research.