Announcements
- It's been a good semester! Enjoy your break.
Overview
This is a course on using proof assistants to build provably correct software:
software accompanied by a formal proof of correctness. Normally,
the word “proof“ means an informal English argument, but in this course, a proof is an
explicit formal object constructed using a proof assistant. The proof assistant
mechanically checks that each step in the proof is valid.
Students learn to use the Coq proof assistant and use it to do a
project in which the properties of some software system or language
are formally modeled and proved.
Students will also read and discuss papers related to
certified software.
Instructors: Greg Morrisett and Andrew Myers
Course information
Course Staff
Placeholder for staff
Prerequisites
CS 6110 or permission of the instructor.
Coursework and Evaluation
Coursework will consist of problem sets, in-class exercises, reading topical research papers and
discussing them in class, and a final project done with a partner.
Students will be evaluated based on class participation, assignments, and their final project.
Placeholder for schedule
Resources
Coq
is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs. Typical
applications include the certification of properties of programming languages
(e.g. the CompCert compiler certification project, or the Bedrock verified
low-level programming library), the formalization of mathematics (e.g. the full
formalization of the Feit-Thompson theorem or homotopy type theory) and
teaching.
The Coq Integrated Development Environment (coqide) is a graphical development
environment for Coq. It allows the user to navigate within a Coq vernacular
file, executing corresponding commands or undoing them respectively.
An Emacs-based generic front-end for proof assistants.
Some nice slides showing what the most useful Coq tactics do.
Topics include basic concepts of logic, computer-assisted theorem proving, the
Coq proof assistant, functional programming, operational semantics, Hoare
logic, and static type systems. The exposition is intended for a broad range of
readers, from advanced undergraduates to PhD students and researchers. No
specific background in logic or programming languages is assumed, though a
degree of mathematical maturity will be helpful.
Other readings
-
Hacker-proof code.
CACM, 60(8):12-14, Aug 2017. E Shein.
-
Using Formal Methods to Eliminate Exploitable Bugs
(video)
USENIX 2015. K Fisher.
-
Social processes and proofs of theorems and programs. CACM 22(5), 1979.
RA De Millo, RJ Lipton, AJ Perlis.
-
How to believe a machine-checked proof. 1997. R Pollack.
-
A formally verified compiler back-end.
J. Automated Reasoning, 2009. X Leroy.
-
seL4: formal verification of an OS kernel
SOSP'09. G Klein, K Elphinstone, G Heiser, J Andronick, D Cock, P Derrin, D
Elkaduwe, K Engelhardt, R Kolanski, M Norrish, T Sewell, H Tuch, S Winwood.
-
Certified software.
CACM, 53(12), Dec 2010. Z Shao.
-
Verdi: A framework for implementing and formally verifying distributed systems.
PLDI'15. JR Wilcox, D Woos, P Panchekha, Z Tatlock, X Wang, MD Ernst, T Anderson.
-
Using Crash Hoare logic for certifying the FSCQ file system.
SOSP'15.
H Chen, D Ziegler, T Chajed, A Chlipala, MF Kaashoek, N Zeldovich.
-
RockSalt: Better, Faster, Stronger SFI for the x86.
PLDI 2012. G Morrisett, G Tan, J Tassarotti, J-B Tristan, E Gan.
-
The Foundational Cryptography Framework.
POST'15. A Petcher, G Morrisett.
-
CertiKOS: An extensible architecture for building certified concurrent OS kernels.
OSDI'16. R Gu, Z Shao, H Chen, X Wu, J Kim, V Sjöberg, D Costanzo.
-
Parametric Higher-Order Abstract Syntax for Mechanized Semantics.
ICFP'08. A Chlipala.
