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

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.

Course requirements

The course has two main requirements:

Grading

The final grade will be composed as follows:

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
Tr 1/27 Induction