|
Computer Science 595
Advanced Topics in Software Systems: Automated Theorem Proving
Andrew W. Appel
|
Fall 2007
|
General Information
Schedule & detailed syllabus
How to build machine-checked proofs about the safety and correctness of software applications and of programming languages and compilers.
Classes: Monday & Wednesday 1:30-2:50, Room: 301
Professor: Andrew W. Appel - 409 CS Building - 258-4627
appel@cs.princeton.edu
Prerequisite: (may be taken simultaneously) COS 441 Programming Languages
Syllabus
Theme 1: Practical Logic.
This will be a hands-on course using the Coq theorem prover.
I will start with a very simple machine model, and cover,
how to specify operational semantics and a type system;
how to build machine checked proofs about the operational semantics and type system.
Readings for this part include:
Theme 2: Writing and reading about machine-checked proofs.
We will study some recent work by researchers who have constructed
machine-checked proofs about programming models and written readable
papers:
- A constructive denotational semantics for Kahn networks in Coq, by Paulin-Mohring, 2007. (See also Kahn 1974)
- Engineering formal metatheory, by Aydemir, Chargueraud, Pierce, Pollack, and Weirich, 2007.
- A
very modal model of a modern, major, general type system, by Appel, Mellies, Richards, and Vouillon, 2007.
- Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, by Leroy, 2006.
-
Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves by Rideau, Serpette, and Leroy, 2007.
Theme 3:
Introduction to the programming-languages
research conducted at Princeton.
- In the style of David August's
research group, how to make a more efficient flow analysis using
Procedure-Boundary Elimination
- In the style of David Walker's research
group, assume that the machine can make mistakes (transient faults),
and use a fault-tolerant type system to guarantee that the software
is resilient.
- In the style of Andrew Appel's research group,
see above ("very modal model...").
Readings
The Bertot and Casteran book is on sale at the U-Store and on reserve at the Engineering Library.
Coq Documentation is on-line.
Logic in Computer Science: Modelling and Reasoning About Systems, 2nd Edition, by Huth and Ryan. Cambridge University Press, 2004.
(On reserve at the Engineering Library)