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 Proof Assistant
- Coq Integrated Development Environment (CoqIDE)
- Proof General
- Coq Survival Kit
- Software Foundations
- Verified Functional Algorithms
- Formal Reasoning about Programs
- Other readings
The Coq Proof Assistant
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.
Coq Integrated Development Environment
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.
Proof General
An Emacs-based generic front-end for proof assistants.
Coq Survival Kit (Pichardie and Blazy)
Some nice slides showing what the most useful Coq tactics do.
Software Foundations (Pierce et al.)
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.
Verified Functional Algorithms (Appel)
Certified Programming with Dependent Types (Chlipala)
Formal Reasoning about Programs (Chlipala)
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.
Assignments
- Problem Set 0: Basic Functional programming in Coq (due 8/31, source code available on CMSX)
- Problem Set 1: Logic and Tactics (due 9/5, source code available on CMSX)
- Problem Set 2: Induction, Equality, and More (due 9/11, source code available on CMSX)
- Problem Set 3: IMP semantics (due 9/22, source code available on CMSX)
- Problem Set 4: Big- vs. Small-step (due 10/6, source code available on CMSX [updated 10/1])
- Problem Set 5: Verifying functional algorithms (due 10/19, source code available on CMSX)