CS 599 G1 - Spring 2022 - Formal Proofs about Programs


Lecture time and location: Tu-Th 11:00-12:15pm - CAS B06A
Instructors: Arthur Azevedo de Amorim and Marco Gaboardi
e-mail: arthur.aa@gmail.com and gaboardi@bu.edu

Office Hours: on Zoom by appointment
Discussion forums: Piazza
Reading material: Software Foundations
Software: Coq
Submission of Assignments: Gradescope

Overview

This course will introduce techniques for formal reasoning about programs and specifications. These techniques are fundamental to ensure that programs are correct and reliable. Bugs and insecurities in software have a huge societal cost, but ensuring programs correctness and reliability in practice is difficult. To assist programmers with this task, researcher in programming languages and software engineering have developed tools based on formal logic. The rigor of formal logic is useful to provide a formal specification for the program behaviour and to check, assisted by a machine, that the program meets this formal specification.

To introduce students to formal reasoning about programs and the basic techniques behind it we will use the Coq proof assistant and we will follow the approach developed in the online book Software Foundations. The precise schedule of the different classes will appear below.

Course prerequisites

The course has a significant component based on analysis of algorithms and systems, and formal techniques. So, the following are required classes: CAS CS 210, CAS CS 320 or equivalent; or consent of instructor. Additionally, some rudimentary understanding of formal logic is expected.

Graduate students

This class satisfy the software breadth requirement for graduate students.

Course requirements

The course has two main requirements:

Assignments

Weekly assignments will be posted on Thursday after class, and will be due the subsequent Thursday before class. Each assignment will consist of exercises taken from the Software Foundations chapters, possibly accompanied by extra exercises that do not appear in the book. In Software Foundations, each exercise is marked on the book with a comment header of the form (* **** Exercise: ...).

Important There are two tracks to this course: advanced and standard. If you are on the standard track, you only need to submit solutions to exercises marked as "standard"; otherwise, if you are on the advanced track, you need to submit solutions to both "standard" and "advanced" exercises. In either case, you do not need to do exercises marked as "optional".

Important Do not change the name of the Coq files when submitting them on Gradescope.

Assignments will be submitted on Gradescope, and each exercise will be graded differently based on its difficulty, as explained in the Preface of Software Foundations.

Grading

The final grade will be composed as follows:

All assignments will have the same weight.

Academic Integrity

As a reminder, the solutions to the programming assignments must be your own. No pair or group submission is allowed. To incentivize academic integrity for the class the instructors reserve the option to regrade a student assignment after inspection of the submission and after discussing the submitted solution with the student.

The Department of Computer Science takes the academic integrity of all students seriously. In order to uphold the integrity of our programs and the university, we rely on students to behave appropriately and take responsibility for their mistakes. Please review the following pages to better understand the expectations of the department, college, and university, as well as the process of any academic misconduct matters.

Class material

The class will be based on the online book serie Software Foundations. Discussion about all the aspects of the course will also take place on Piazza.

Software

In class and in the assignments we will use the proof assistant Coq. We recommend to install Coq using the Coq platform. More information are available here https://coq.inria.fr/download. We have also created a post on piazza to discuss problems with the installation that you may encounter.

Lecture Schedule

Date Topic Notes
Tr 1/20 No Class
Tu 1/25 Introduction to the topic + Use of Coq + Basics
Basics
Tr 1/27 More Basics
Basics
Tu 2/1 Proof by Induction
Induction
Th 2/3 Working with Structured Data
Lists
Tu 2/8 Polymorphism and Higher-Order Functions
Poly
Th 2/10 More Basic Tactics
Tactics
Th 2/15 More Basic Tactics
Tactics

Homework

Due Date Name Required exercises Files
Tr 2/3, 10am Hw 1
All the non-optional exercises in this chapter Basics.v
Tr 2/10, 10am Hw 2
All the non-optional exercises in these chapters except for add_comm_informal in Induction and add_inc_count in Lists Induction.v Lists.v
Tr 2/17, 10am Hw 3
All the non-optional exercises in this chapters except for fold_length, nth_error_informal and church_exp. Poly.v PolyTest.v