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
Lectures: Tuesdays and Thursdays 3:05PM - 4:20PM at Sackett Bldg 324.
|| 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:
- Software Foundations by Piece et al. Download the book here and use
your browser to open toc.html. Note that this version of the book is different from
the version you can find online.