CS 4160 Spring 2020 Syllabus

Professor: Michael Clarkson (Cornell PhD 2010)

Graduate Teaching Assistant: Matvey Soloviev (ms2837)

Undergraduate Teaching Assistants: Deva Devanandan (rd473), Pierce Douglis (pad227), Tjaden Hess (tah83), Natalie Neamtu (nan55), Dylan Tsai (dt439), Amanda Xu (ax49)

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.

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 led by Benjamin C. Pierce at 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 most of volume 3.

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.

We will have a preliminary exam (prelim) and a final, each of which will cover about half the course. These will be take-home exams that involve writing programs and proving theorems in Coq, just like the assignments.

Announcements and Q&A

We will use Campuswire for announcements and online Q&A. You need a PIN to register yourself in the Campuswire class; that PIN is available in CMS.

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. Last year, the median grade was in fact an A.

Your lowest assignment grade excluding the last assignment will be dropped. If you joined the class late hence missed submitting some initial assignments, those will be dropped instead.

Course Policies

Assignments: The policies on assignments (including late submissions, extensions, regrades, etc.) have been factored out into a separate page.

Academic Integrity: The Cornell University Code of Academic Integrity and the Computer Science Department Code of Academic Integrity are in effect. In addition to those policies, we add these course-specific policies:

Accommodations and Mental Health

Your mental health is important. If there are struggles you are facing, we hope that you seek help; several resources are listed on this page. The professor is happy to have a private conversation with you—just drop by, no appointment necessary—if you ever just need to talk.

If you need ongoing accommodations in this course for reasons of mental health, there are three ways to make that happen. The first is for Student Disability Services (SDS) to issue a letter on your behalf. The second is for your college’s advising staff to issue a Request for Academic Consideration on your behalf (which might be based on you asking your CAPS counselor to contact your college advising staff). The third is for a private health care professional to write a letter on your behalf. Note that Cornell Health will usually decline to write letters, but will instead to prefer to work through your college advising staff.

Accommodation requests need to be made as soon as possible, so that there is time to work out the logistics. Last-minute accommodation requests (such as, “I can’t submit this assignment by tomorrow” or “I can’t take the exam tomorrow”) due to procrastination are very problematic.

For emergent issues, including sudden medical and mental health crises, temporary considerations will be arranged by the professor to help you meet course requirements. But for ongoing concerns, you are encouraged to seek consultation with CAPS, your academic advisor, and/or your advising dean.

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]