CS 4160 Spring 2019 Syllabus

Professor: Michael Clarkson (Cornell PhD 2010)

Teaching Assistants: Samantha Deng, Tjaden Hess, Devin Lehmacher, Devin Smedira, Weiyu Wang

Catalog Description: An introduction to formal verification, focusing on correctness of functional and imperative programs relative to mathematical specifications. Topics include computer-assisted theorem proving, logic, programming language semantics, and verification of algorithms and data structures. Assignments involve extensive use of a proof assistant to develop and check proofs. Prerequisite: CS 3110 or permission of instructor.

Lecture: TuTh 2:55–4:10 in Hollister B14, starting January 22, 2019.

Table of Contents:

Am I Right?

How do you know whether a program is correct?

Programming is taught by inductive reasoning: beginning programmers are shown examples of programs, from which they generalize and learn to write other programs [1]. Program testing is likewise a process of inductive reasoning. Programmers write test cases, and after gathering enough evidence that the program is correct (whatever “evidence” and “correct” might mean), they declare success. “Am I right?” asks the programmer. “Maybe” is the best answer that can be given.

Deductive reasoning offers an alternative [2]. The correctness of a program can be logically deduced from its specification according to rules of inference, a task known as formal verification. This is not a simple task! But for programs that must be dependable—control software for avionics, algorithms hardcoded into CPUs, medical systems, security subsystems, etc.—it can be a worthwhile task. “Am I right?” asks the programmer. “Yes” or “no” can now be answered with assurance.

Formal verification does not necessarily require a computer, though. We could (as it was done in the 1970s) write programs on paper and prove their correctness, also on paper. That approach does not scale well. Instead, the computer itself can help us construct proofs. So we move from proof about computers to proof with computers.

This purpose of this course is to investigate how to answer the question, “Am I right? i.e., is my program correct?”, using formal verification aided by the computer. We will use the Coq proof assistant to verify the correctness of functional and imperative programs relative to mathematical specifications. Along the way we’ll learn (more) about logic and programming language semantics.

The world has too much buggy software. Let’s make it right.

Citations.

  1. Edward Cohen, Programming in the 1990s, Springer-Verlag, 1990, p. vi. Cohen was a student of Prof. David Gries here at Cornell.

  2. Donald MacKenzie, Mechanizing Proof, MIT Press, 2001, p. 2.

What We Will Do to Pursue that Question

An international group of researchers spearheaded by Prof. Benjamin C. Pierce at the University of Pennsylvania (UPenn) has been creating an online textbook series titled Software Foundations (SF). The series describes itself as

a broad introduction to the mathematical underpinnings of reliable software. The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a “proof script” for the Coq proof assistant.

We will follow a path through SF in pursuit of an answer to our question of how to formally verify software: most of volume 1, a little bit of volume 2, and as much of volume 3 as we can get through.

Each week we will cover some chapters of SF in class. You will then do the exercises in those chapters as individual assignments. Some exercises involve writing free-form answers in English or standard mathematical proofs. But most exercises will involve writing programs and proving theorems with Coq. There will be no partial credit on Coq exercises, which is in part because of the nature of this course. Formal verification is about getting it right. Either Coq accepts your proof, or it rejects it. You will know which case you’re in before you submit, so there should not be any surprises in grading.

We will have a preliminary exam (prelim) and a final, each of which will cover about half the course. The exams will involve answering questions on paper, and might also include an in-class or take-home component that involves writing programs and proving theorems in Coq.

Announcements and Q&A

We will use Campuswire (instead of Piazza) for announcements and online Q&A. You need a PIN to register yourself in the Campuswire class; that PIN will be announced during the first lecture and in CMS.

Polling

We will use Poll Everywhere for in-class polls. There is no additional charge to you for that service; you just need to have a device that is connected to the Internet, or a mobile phone that can send text messages.

Grades

We expect the breakdown for the final course score to be as follows:

How that score will be transformed into a final letter grade is not based on any pre-determined curve or point cutoffs. We’d be happy for everyone to get A’s, if everyone demonstrated excellent mastery of the material.

Course Policies

Academic Integrity: The Cornell University Code of Academic Integrity and the Computer Science Department Code of Academic Integrity are in effect.

Late Submissions: Assignments are due at the deadline given in CMS. But, to give you flexibility in managing your work schedule, late submissions will be then accepted at no penalty until the late submission deadline given in CMS (usually, that will be 48 hours). After the late submission deadline expires, no further submissions will be accepted. Be aware that CMS does not allow any grace period for the late submission deadline, so you must be careful to submit well before it. If you accidentally miss the late submission deadline, recall that your lowest assignment score will be dropped, thus mitigating that mistake (once).

Extensions: Additional time beyond the 48 hours already provided will be granted only in truly exceptional circumstances. Extension requests require accompanying documentation: a letter from a Cornell professor, advisor, or coach requesting the extension on your behalf; an obituary or wedding announcement published in a newspaper; or a letter on official letterhead from a medical provider explaining a major illness or injury. Contact the professor to request an extension.

Regrades and Appeals: If there is something you don’t understand about your grading comments, speak with the grader. If you still disagree with your grade, you may appeal to the professor.

A Final Thought

We wish [students] good luck in their discovery of a difficult but exciting world—may their efforts be rewarded by the joy of the last QED, an end to weeks and sometimes months of adamant but still unconcluded toil, the final touch that validates the whole enterprise. [Gérard Huet and Christine Paulin-Mohring in the foreword to Interactive Theorem Proving and Program Development by Yves Bertot and Pierre Castéran, Springer, 2004]