Course Summary

The course covers the state of the art of interactive theorem proving and static-analysis techniques. The first part of the course will use an interactive theorem prover such as Coq to teach the basics about how to develop machine-checked proofs about the correctness of computer systems. Applications in programming languages, compilers, security, and operating systems will also be covered. The second part will cover the foundation of static analysis such as abstract interpretation as well as its wide-range applications in security and programming languages.

Prerequisites: CMPSC 461 (Programming Language Concepts) and CMPSC 464 (Theory of Computation), or equivalent classes in other universities.


Administrative Information

Lectures: Tuesdays and Thursdays 3:05PM - 4:20PM at Sackett Bldg 324.

Professor: Gang Tan; 346C IST Building; phone: 814-8657364; gtan at cse dot psu dot edu
Office hours: Weds 2-3pm, or by appointment

Syllabus: See the [PDF] file.

Textbook: not required, but we will work through the following online resources: