CMSC631: Program Analysis and Understanding

Fall, 2022

The objective of this course is to introduce students to programming languages with a particular emphasis on formal verification and random testing. 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.