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.
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.
This class satisfy the software breadth requirement for graduate students.
The course has two main requirements:
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.
The final grade will be composed as follows:
All assignments will have the same weight.
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.
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.
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.
| 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
|
| 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 |