### Course Description

Software correctness is typically established through exhaustive testing. A
Python program which has never been executed on examples is likely full of
bugs, even if it was translated from a correct on-paper algorithm. Software
verification is the process of eliminating large classes of bugs from software
such that testing is no longer necessary to gain confidence in its quality.

Software verification is particularly attractive for situations where the
software is difficult to test (e.g., parallel and quantum algorithms), or where
absolute correctness is critical (e.g., control code for airplanes). However,
verification only rules out bugs *for the property which has been verified*.
Because of this, there will always be situations where testing techniques are
preferred-to (or complimentary-to) verification techniques. In particular,
testing techniques are essential for properties which are challenging or
impossible to specify formally. (E.g., what is the specification for a website
to be “user-friendly” or for a game to be “fun”?)

In this course we will study advanced methods for software verification.
Software verification can mean many things—from “lightweight” verification,
such as verifying the absence of simple type errors, to “middleweight”
verification, such as verifying the absence of buffer overflows or runtime
exceptions, to “heavyweight” verification, such as verifying the full
functional correctness of a C compiler. We will study this entire spectrum of
verification, with a sharper focus on the following topics: (1) specification
design, both deep and shallow; (2) automation and semi-automation techniques in
verification; and (3) correct-by-construction software design. 

We will explore verification topics through a tool called a *proof assistant*.
Proof assistants allow the embedding of programs within the tool, as well as
constructing proofs of correctness about the embedded programs. The default
mode of verification for the tool is manual and interactive, however full
automation of correctness proofs can also be achieved. After constructing the
proof of correctness for a piece of software, one then “extracts” an
executable, certified program from the tool environment. It is also possible to
mix computation and logical fragments of the tool, which can lead to a more
correct-by-construction process for certified software design.

The course will consist primarily of programming assignments using a proof
assistant. There will be a final project at the end of the course where
students will verify a medium-sized program of their choice.

Here is an excerpt from the introduction to the Software Foundations series
which will be used in the latter part of the course:

> Building reliable software is really hard. The scale and complexity of modern
> systems, the number of people involved, and the range of demands placed on
> them make it extremely difficult to build software that is even more-or-less
> correct, much less 100% correct. At the same time, the increasing degree to
> which information processing is woven into every aspect of society greatly
> amplifies the cost of bugs and insecurities.
>
> Computer scientists and software engineers have responded to these challenges
> by developing a whole host of techniques for improving software reliability,
> ranging from recommendations about managing software projects teams (e.g.,
> extreme programming) to design philosophies for libraries (e.g.,
> model-view-controller, publish-subscribe, etc.) and programming languages
> (e.g., object-oriented programming, aspect-oriented programming, functional
> programming, ...) to mathematical techniques for specifying and reasoning
> about properties of software and tools for helping validate these properties.
> The Software Foundations series is focused on this last set of techniques.
>
> The text is constructed around three conceptual threads: (1) basic tools from
> logic for making and justifying precise claims about programs; (2) the use of
> proof assistants to construct rigorous logical arguments; (3) functional
> programming, both as a method of programming that simplifies reasoning about
> programs and as a bridge between programming and logic.

**Prerequisites:** CS 124 (Data Structures and Algorithms) and CS 125
(Computability and Complexity)

**Recommended (but not required):** CS 225 (Programming Languages)

### Administration

**Lecture:** Tuesdays and Thursdays, 10:05–11:20am, Morrill Hall 010   
**Instructor:** [David Darais](http://david.darais.com)   
**Office Hours:** Wednesdays, 1:30–3:30pm, Votey 319

**TAs:** Walter (my dog)   
![Walter](images/walter.jpg)

**Course Piazza:** [CS 295A: Software Verification](https://piazza.com/class#spring2018/cs295A)   
*Course announcements and discussion will take place on Piazza exclusively.*

### Textbook

We will use [Kokke and Wadler's Programming Language Foundations in Agda][PLFA]
and [Pierce et al's Software Foundations Series][SF]. All books are freely
available online. We will follow Kokke and Wadler's book closely for the first
half of the class, and the Software Verification volume of Pierce et al's
series (written by Appel) loosely for the last half of the class. Some homework
problems will be drawn directly from these textbooks.

[PLFA]: https://plfa.github.io
[SF]: https://softwarefoundations.cis.upenn.edu

### Software Tools

Throughout the course we will use the [Agda][Agda] programming language and proof
assistant. For the first assignment you will be required to successfully set up
and configure Agda on your personal machine. We will use Agda v2.5.4.1. A
virtual appliance which has Agda installed and configured will also be
provided.

[Agda]: https://agda.readthedocs.io

You will know your grade for each assignment before submitting. This is because
Agda is capable of not just running your code, but also checking your work for
correctness. If your assignment passes Agda's checker, you are guaranteed a
100% on the assignment.

- [Agda setup](agda-setup.html)
- [Agda documentation](https://agda.readthedocs.io)
- [Agda-mode commands and unicode input](https://agda.readthedocs.io/en/v2.5.4.1/tools/emacs-mode.html)
- [All Agda-mode Unicode](https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el)
- ⦗[Basics-v1-A][]⦘ ⦗[Basics-v1-H][]⦘
- ⦗[Basics-v2-A][]⦘ ⦗[Basics-v2-H][]⦘
- ⦗[Basics-v3-A][]⦘ ⦗[Basics-v3-H][]⦘
- ⦗[Basics-v4-A][]⦘ ⦗[Basics-v4-H][]⦘
- ⦗[Basics-v5-A][]⦘ ⦗[Basics-v5-H][]⦘
- ⦗[Basics-v6-A][]⦘ ⦗[Basics-v6-H][]⦘

[Basics-v1-A]: basics/Basics-v1.agda
[Basics-v1-H]: basics/html/Basics-v1.html
[Basics-v2-A]: basics/Basics-v2.agda
[Basics-v2-H]: basics/html/Basics-v2.html
[Basics-v3-A]: basics/Basics-v3.agda
[Basics-v3-H]: basics/html/Basics-v3.html
[Basics-v4-A]: basics/Basics-v4.agda
[Basics-v4-H]: basics/html/Basics-v4.html
[Basics-v5-A]: basics/Basics-v5.agda
[Basics-v5-H]: basics/html/Basics-v5.html
[Basics-v6-A]: basics/Basics-v6.agda
[Basics-v6-H]: basics/html/Basics-v6.html

### Policies

**Grades:** Your grade for the course will be calculated as follows: 80%
Assignments (10 assignments at 8% each assignment), and 20% Final Project. 
You are guaranteed a 100% on your assignment if it passes the Agda type
checker.

**Late Work:** Each assignment will be released after class on a Thursday and
due before class one week later. Late work will not be accepted.

**Collaboration:** Collaboration on the high-level ideas and approach on
assignments is encouraged. Copying someone else's work is not allowed. Any
collaboration, even at a high level, must be declared when you submit your
assignment. Every assignment must include a collaboration statement. E.g., “I
discussed high-level strategies for solving problem 2 and 5 with Alex.”
Students caught copying work are eligible for immediate failure of the course
and disciplinary action by the University. All academic integrity misconduct
will be treated according to [UVM's Code of Academic Integrity][UVM-CAI].

[UVM-CAI]: https://www.uvm.edu/policies/student/acadintegrity.pdf

**Small Group Assignments:** For homeworks 6–10 you will be allowed to work in
groups of size 1–2 (independently or in pairs). You may submit a single
solution to the assignment for 2-person groups. There will be more detailed
instructions about how to submit groupwork in the assignment writeup.

**Final Group Project:** For the final project, you will be allowed to work in
groups of size 1–4, however I will expect a larger amount of work to be
completed as group size increases.

### Schedule

Date        | Topic                                                                              | Homework                       
------------|------------------------------------------------------------------------------------|-------------------------------------
Tue, Aug 28 | Welcome ⅋ Overview ⦗[LH1][]⦘                                                       |                                
Thu, Aug 30 | Intro to Verification ⦗[LH2][]⦘                                                    |                                
Tue, Sep 04 | PLFA: Naturals  ⦗[IC3-A][]⦘ ⦗[IC3-H][]⦘ ⦗[LA3-A][]⦘ ⦗[LA3-H][]⦘                    |                                
Thu, Sep 06 | PLFA: Induction ⦗[IC4-A][]⦘ ⦗[IC4-H][]⦘ ⦗[LA4-A][]⦘ ⦗[LA4-H][]⦘                    | HW1 ⦗[HW1-A][]⦘ ⦗[HW1-H][]⦘ ⦗[SL1-H][]⦘
Tue, Sep 11 | PLFA: Relations 1 ⦗[IC5-A][]⦘ ⦗[IC5-H][]⦘ ⦗[LA5-A][]⦘ ⦗[LA5-H][]⦘                  |                                
Thu, Sep 13 | PLFA: Relations 2 ⦗[IC6-A][]⦘ ⦗[IC6-H][]⦘ ⦗[LA6-A][]⦘ ⦗[LA6-H][]⦘                  | HW1 Due ⌁ HW2 Release ⦗[HW2-A][]⦘ ⦗[HW2-H][]⦘ ⦗[SL2-H][]⦘
Tue, Sep 18 | PLFA: Connectives ⦗[IC7-A][]⦘ ⦗[IC7-H][]⦘ ⦗[LA7-A][]⦘ ⦗[LA7-H][]⦘                  |                                
Thu, Sep 20 | PLFA: Negation ⅋ Quantification ⦗[IC8-A][]⦘ ⦗[IC8-H][]⦘ ⦗[LA8-A][]⦘ ⦗[LA8-H][]⦘    | HW2 Due ⌁ HW3 Release ⦗[HW3-A][]⦘ ⦗[HW3-H][]⦘ ⦗[SL3-H][]⦘
Tue, Sep 25 | *No Class*                                                                         |                                
Thu, Sep 27 | *No Class*                                                                         | HW3 Due ⌁ HW4 Release ⦗[HW4-A][]⦘ ⦗[HW4-H][]⦘ ⦗[SL4-H][]⦘
Tue, Oct 02 | PLFA: Decidable ⦗[IC9-A][]⦘ ⦗[IC9-H][]⦘  ⦗[LA9-A][]⦘ ⦗[LA9-H][]⦘                   |                                
Thu, Oct 04 | PLFA: Lists ⦗[IC10-A][]⦘ ⦗[IC10-H][]⦘ ⦗[LA10-A][]⦘ ⦗[LA10-H][]⦘                    | HW4 Due ⌁ HW5 Release ⦗[HW5-A][]⦘ ⦗[HW5-H][]⦘ ⦗[SL5-H][]⦘
Tue, Oct 09 | Type Classes ⅋ Insertion Sort ⦗[IC11-A][]⦘ ⦗[IC11-H][]⦘ ⦗[LA11-A][]⦘ ⦗[LA11-H][]⦘  |                                
Thu, Oct 11 | Selection Sort ⦗[IC12-A][]⦘ ⦗[IC12-H][]⦘ ⦗[LA12-A][]⦘ ⦗[LA12-H][]⦘                 | HW5 Due ⌁ HW6 Release ⦗[HW6-A][]⦘ ⦗[HW6-H][]⦘ ⦗[SL6-H][]⦘
Tue, Oct 16 | Termination and Merge Sort ⦗[IC13-A][]⦘ ⦗[IC13-H][]⦘ ⦗[LA13-A][]⦘ ⦗[LA13-H][]⦘     |                                
Thu, Oct 18 | Well Founded Induction ⦗[IC14-A][]⦘ ⦗[IC14-H][]⦘  ⦗[LA14-A][]⦘ ⦗[LA14-H][]⦘        | HW6 Due ⌁ HW7 Release ⦗[HW7-A][]⦘ ⦗[HW7-H][]⦘ ⦗[SL7-H][]⦘
Tue, Oct 23 | Permutation and Ordering ⦗[IC15-A][]⦘ ⦗[IC15-H][]⦘ ⦗[LA15-A][]⦘ ⦗[LA15-H][]⦘       |                                
Thu, Oct 25 | Intro Red Black Trees ⦗[IC16-A][]⦘ ⦗[IC16-H][]⦘ ⦗[LA16-A][]⦘ ⦗[LA16-H][]⦘          | HW7 Due ⌁ HW8 Release ⦗[HW8-A][]⦘ ⦗[HW8-H][]⦘ ⦗[SL8-H][]⦘
Tue, Oct 30 | 2-3 Trees  ⦗[IC17-A][]⦘ ⦗[IC17-H][]⦘ ⦗[LA17-A][]⦘ ⦗[LA17-H][]⦘                     |                                
Thu, Nov 01 | 2-3 Trees Insertion ⦗[IC18-A][]⦘ ⦗[IC18-H][]⦘ ⦗[LA18-A][]⦘ ⦗[LA18-H][]⦘            | HW8 Due ⌁ HW9 Release ⦗[HW9-A][]⦘ ⦗[HW9-H][]⦘
Tue, Nov 06 | Vectors, Matrices and Graph ⦗[IC19-A][]⦘ ⦗[IC19-H][]⦘                              |                                
Thu, Nov 08 | Depth First Search ⦗[IC19-A][]⦘ ⦗[IC19-H][]⦘                                       | HW9 Due ⌁ HW10 Release ⦗[HW10-A][]⦘ ⦗[HW10-H][]⦘
Tue, Nov 13 | Variables and Embedded Languages                                                   |                                
Thu, Nov 15 | Solving Monoid Equations                                                           | HW10 Due                       
Thu, Nov 20 | *Thanksgiving Recess*                                                              |                                
Thu, Nov 22 | *Thanksgiving Recess*                                                              |                                
Tue, Nov 27 | Reflective Tactics in Agda                                                         |                                
Thu, Nov 29 | Case Study: Liquid Agda                                                            |                                
Tue, Dec 04 | Case Study: Liquid Agda                                                            |                                
Thu, Dec 06 | Final Project Presentations                                                        | Final Project Due              

[LH1]: lh/lh1.html
[LH2]: lh/lh2.html

[IC3-A]: ic/ic3.agda
[IC4-A]: ic/ic4.agda
[IC5-A]: ic/ic5.agda
[IC6-A]: ic/ic6.agda
[IC7-A]: ic/ic7.agda
[IC8-A]: ic/ic8.agda
[IC9-A]: ic/ic9.agda
[IC10-A]: ic/ic10.agda
[IC11-A]: ic/ic11.agda
[IC12-A]: ic/ic12.agda
[IC13-A]: ic/ic13.agda
[IC14-A]: ic/ic14.agda
[IC15-A]: ic/ic15.agda
[IC16-A]: ic/ic16.agda
[IC17-A]: ic/ic17.agda
[IC18-A]: ic/ic18.agda
[IC19-A]: ic/ic19.agda

[IC3-H]: ic/html/ic3.html
[IC4-H]: ic/html/ic4.html
[IC5-H]: ic/html/ic5.html
[IC6-H]: ic/html/ic6.html
[IC7-H]: ic/html/ic7.html
[IC8-H]: ic/html/ic8.html
[IC9-H]: ic/html/ic9.html
[IC10-H]: ic/html/ic10.html
[IC11-H]: ic/html/ic11.html
[IC12-H]: ic/html/ic12.html
[IC13-H]: ic/html/ic13.html
[IC14-H]: ic/html/ic14.html
[IC15-H]: ic/html/ic15.html
[IC16-H]: ic/html/ic16.html
[IC17-H]: ic/html/ic17.html
[IC18-H]: ic/html/ic18.html
[IC19-H]: ic/html/ic19.html

[LA3-A]: la/la3.agda
[LA4-A]: la/la4.agda
[LA5-A]: la/la5.agda
[LA6-A]: la/la6.agda
[LA7-A]: la/la7.agda
[LA8-A]: la/la8.agda
[LA9-A]: la/la9.agda
[LA10-A]: la/la10.agda
[LA11-A]: la/la11.agda
[LA12-A]: la/la12.agda
[LA13-A]: la/la13.agda
[LA14-A]: la/la14.agda
[LA15-A]: la/la15.agda
[LA16-A]: la/la16.agda
[LA17-A]: la/la17.agda
[LA18-A]: la/la18.agda
[LA19-A]: la/la19.agda

[LA3-H]: la/html/la3.html
[LA4-H]: la/html/la4.html
[LA5-H]: la/html/la5.html
[LA6-H]: la/html/la6.html
[LA7-H]: la/html/la7.html
[LA8-H]: la/html/la8.html
[LA9-H]: la/html/la9.html
[LA10-H]: la/html/la10.html
[LA11-H]: la/html/la11.html
[LA12-H]: la/html/la12.html
[LA13-H]: la/html/la13.html
[LA14-H]: la/html/la14.html
[LA15-H]: la/html/la15.html
[LA16-H]: la/html/la16.html
[LA17-H]: la/html/la17.html
[LA18-H]: la/html/la18.html
[LA19-H]: la/html/la19.html

[HW1-A]: hw/hw1.agda
[HW2-A]: hw/hw2.agda
[HW3-A]: hw/hw3.agda
[HW4-A]: hw/hw4.agda
[HW5-A]: hw/hw5.agda
[HW6-A]: hw/hw6.agda
[HW7-A]: hw/hw7.agda
[HW8-A]: hw/hw8.agda
[HW9-A]: hw/hw9.agda
[HW10-A]: hw/hw10.agda

[HW1-H]: hw/html/hw1.html
[HW2-H]: hw/html/hw2.html
[HW3-H]: hw/html/hw3.html
[HW4-H]: hw/html/hw4.html
[HW5-H]: hw/html/hw5.html
[HW6-H]: hw/html/hw6.html
[HW7-H]: hw/html/hw7.html
[HW8-H]: hw/html/hw8.html
[HW9-H]: hw/html/hw9.html
[HW10-H]: hw/html/hw10.html

[SL1-A]: sl/sl1.agda
[SL2-A]: sl/sl2.agda
[SL3-A]: sl/sl3.agda
[SL4-A]: sl/sl4.agda
[SL5-A]: sl/sl5.agda
[SL6-A]: sl/sl6.agda
[SL7-A]: sl/sl7.agda
[SL8-A]: sl/sl8.agda
[SL9-A]: sl/sl9.agda
[SL10-A]: sl/sl10.agda

[SL1-H]: sl/html/sl1.html
[SL2-H]: sl/html/sl2.html
[SL3-H]: sl/html/sl3.html
[SL4-H]: sl/html/sl4.html
[SL5-H]: sl/html/sl5.html
[SL6-H]: sl/html/sl6.html
[SL7-H]: sl/html/sl7.html
[SL8-H]: sl/html/sl8.html
[SL9-H]: sl/html/sl9.html
[SL10-H]: sl/html/sl10.html

Last updated Oct 4 30, 2018