## Announcements

- Check Piazza for announcements.

## 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.
- 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.
- The Foundational Cryptography Framework. POST'15. A Petcher, G Morrisett.
- Using Crash Hoare logic for certifying the FSCQ file system. SOSP'15. H Chen, D Ziegler, T Chajed, A Chlipala, MF Kaashoek, N Zeldovich.
- 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.
- A Hammer for Coq, Automation for Dependent Type Theory Łukasz Czajka and Cezary Kaliszyk, 2017.
- Using Formal Methods to Eliminate Exploitable Bugs (video) USENIX 2015. K Fisher.
- Saving the World from Code. The Atlantic, Sept 2017. James Somers.

## 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)