### Catalogue Description

Principles and practice of software specification and verification. Design of
algorithms which are verified correct using interactive or automated
software-based tools. Emphasis on the design space for software specification,
and the spectrum of verification goals ranging from shallow to deep
verification. Includes a course project.

**Learning Outcomes:** Students will learn to (1) craft specifications for
software correctness, (2) design software which can be proven correct w.r.t.
a formal specification, (3) construct machine-checkable proofs of software
correctness using a proof assistant, and (4) work in a collaborative,
group-based project setting where software is specified and verified in small
components and then later assembled in a modular fashion.

### 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. Students taking
this course for graduate credit will be expected to complete a more substantial
final project.

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.

Interest in “heavyweight” verification of software has grown in recent years.
The first major success story was [CompCert][] (2009) by Xavier Leroy: a C
compiler and verification of full functional correctness in the Coq proof
assistant. CompCert rose to fame in part due to Xuejun et al's paper on [Bugs
in C Compilers] and [CSmith] tool (2011) which demonstrated the presence of
bugs in all major C compilers *except* the only compiler that was fully
verified: CompCert. More recently Microsoft Research launched the [Everest][]
project (2016) which aims to fully verify the HTTPS stack (in part motivated by the
[Heartbleed][] bug (2014) in OpenSSL) in (mostly) F*. Also recently is the
[DeepSpec][] project (2016) at Princeton, MIT, UPenn and Yale which aims to
achieve a fully verified OS+Compiler+Runtime ecosystem in (mostly) Coq.

[CompCert]: http://compcert.inria.fr
[Everest]: https://www.microsoft.com/en-us/research/project/project-everest-verified-secure-implementations-https-ecosystem/
[Heartbleed]: http://heartbleed.com
[DeepSpec]: https://deepspec.org/main
[Bugs in C Compilers]: http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf
[CSmith]: https://embed.cs.utah.edu/csmith/

**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, Kalkin Building 001  
**Instructor:** [David Darais](http://david.darais.com)   
**Office Hours:** David Darais — Innovation E456 — at the following times:

- Tuesdays: 4:30–5:00pm
- Wednesdays: 4:30–5:00pm
- Fridays: 1:00–2:00pm

**TAs:** Walter (my dog)   

**Course Piazza:** [CS 295A: Software Verification](https://piazza.com/class#spring2019/cs295A)

- *Course announcements and discussion will take place on Piazza exclusively.*
- *Please use Piazza exclusively for asking for help on homework.*
- *I promise to answer any homework questions that are posted more than 24
  hours before the homework is due.* 
- I will try to answer questions posted less than 24 hours before the deadline
  but make no promises. You should still always post—maybe a classmate can help
  you out!

### Textbook

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

[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 embedded in the [Emacs][Emacs] or (less-supported) [Atom][Atom]
text editors. For the first assignment you will be required to successfully set
up and configure both Emacs (or Atom) and Agda on your personal machine. You
may install these applications directly, or virtualize them, e.g., through a
Ubuntu virtual machine. A virtual machine which has Emacs, Atom and Agda
installed and configured is provided in [Agda Setup][Agda Setup]. We will use
Agda v2.5.4.2. 

[Agda]: https://agda.readthedocs.io
[Emacs]: https://www.gnu.org/software/emacs/
[Atom]: https://atom.io
[Agda Setup]: agda-setup.html

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 Documentation](https://agda.readthedocs.io)
- [Agda-mode](https://agda.readthedocs.io/en/v2.5.4.1/tools/emacs-mode.html)
- [Darais Unicode Input](https://github.com/davdar/dotfiles/tree/master/unicode)
- [Agda Setup](agda-setup.html)
- [Git Info](git-info.html)

### Policies

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

**Late Work:** Each assignment will typically be released after class on a
Thursday and due before class one week later. *Late work will not be accepted.*
There are 10 assignments and I will drop your lowest assignment score; your
best 9 assignments are used to calculate your grade.

**Collaboration:** Collaboration on the high-level ideas and approach on
assignments is encouraged. Copying someone else's work is not allowed. Copying
solutions from an online source is not allowed. Any collaboration or online
resources, even if used only at a high level, must be declared when you submit
your assignment. Every assignment must include a collaboration and resources
statement. E.g., “I discussed high-level strategies for solving problem 2 and 5
with Alex; I found this stackoverflow post helpful while working on problem 3
” 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

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

**Small Group Assignments:** For homeworks 6–10 you may work either
individually or in groups 2. 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–3, however I will expect a larger amount of work to be
completed as group size increases. For group projects, you must identify
up-front relatively isolated parts of the project that each group member is
responsible for.

### In Class Files (.agda)

- [IC3][]
- [IC4][]
- [IC5][]
- [IC6][]
- [IC7][]
- [IC8][]
- [IC9][]
- [IC10][]
- [IC11][]
- [IC12][]

### Assignments (.agda)

- [HW1][HW1-DL]
- [HW2][HW2-DL]
- [HW3][HW3-DL]
- [HW4][HW4-DL]
- [HW5][HW5-DL]
- [HW6][HW6-DL]
- [HW7][HW7-DL]
- [HW8][HW8-DL]
- [HW9][HW9-DL]
- [HW10][HW10-DL]

### Final Project

[Final Project](final-project.html)

### Schedule

Date        | Topic                                             | Homework                       
Tue, Aug 27 | Welcome ⅋ Overview ⦗[LN1][]⦘                      |                                
Thu, Aug 29 | Intro to Verification ⦗[LN2][]⦘                   | HW1 Release ⦗[HW1][]⦘ ⦗SL1⦘                               
Tue, Sep 03 | Intro to Agda ⦗[IC3-SL][]⦘                        |                                
Thu, Sep 05 | Naturals ⅋ Induction 1 ⦗[LN4][]⦘ ⦗[IC4-SL][]⦘     | HW1 Due ⌁ HW2 Release ⦗[HW2][]⦘ ⦗SL2⦘
Tue, Sep 10 | Naturals ⅋ Induction 2 ⦗[LN4][]⦘ ⦗[IC4-SL][]⦘     |                                
Thu, Sep 12 | Order ⅋ Relations 1 ⦗[LN5][]⦘ ⦗[IC5-SL][]⦘        | HW2 Due ⌁ HW3 Release ⦗[HW3][]⦘ ⦗SL3⦘
Tue, Sep 17 | Order ⅋ Relations 2 ⦗[LN5][]⦘ ⦗[IC5-SL][]⦘        |                                
Thu, Sep 29 | Negation ⅋ Quantification 1 ⦗LN6⦘ ⦗[IC6-SL][]⦘    | HW3 Due ⌁ HW4 Release ⦗[HW4][]⦘ ⦗SL4⦘
Tue, Sep 24 | Negation ⅋ Quantification 2 ⦗LN6⦘ ⦗[IC6-SL][]⦘    |                                
Thu, Sep 26 | Lists 1 ⦗[IC7-SL][]⦘                              | HW4 Due ⌁ HW5 Release ⦗[HW5][]⦘ ⦗SL5⦘
Tue, Oct 01 | Lists 2 ⦗[IC7-SL][]⦘                              |                                
Thu, Oct 03 | Insertion and Selection Sort 1 ⦗[IC8-SL][]⦘       | HW5 Due ⌁ HW6 Release ⦗[HW6][]⦘ ⦗SL6⦘
Tue, Oct 08 | Insertion and Selection Sort 2 ⦗[IC8-SL][]⦘       |                                
Thu, Oct 10 | Termination and Merge Sort 1 ⦗[IC9-SL][]⦘         | HW6 Due ⌁ HW7 Release ⦗[HW7][]⦘ ⦗SL7⦘
Tue, Oct 15 | Termination and Merge Sort 2 ⦗[IC9-SL][]⦘         |                                
Thu, Oct 17 | Permutations ⦗[IC10-SL][]⦘                        | HW7 Due ⌁ HW8 Release ⦗[HW8][]⦘ ⦗SL8⦘
Tue, Oct 22 | *No Class*                                        |                                
Thu, Oct 24 | *No Class*                                        | HW8 Due ⌁ HW9 Release ⦗[HW9][]⦘ ⦗SL9⦘
Tue, Oct 29 | Vectors ⅋ Matrices ⦗[IC11-SL][]⦘                  | 
Thu, Nov 31 | Final Project Discussion                          | HW9 Due ⌁ HW10 Release ⦗[HW10][]⦘ ⦗SL10⦘
Tue, Nov 05 | Graphs ⅋ Graph Algorithms ⦗[IC12-SL][]⦘           |                                
Thu, Nov 07 | Git Workflow ⦗LNX⦘                                | 
Tue, Nov 12 | Final Projects                                    | HW10 Due ⌁ Start Final Projects
Thu, Nov 14 | Final Projects (maybe special topic)              | Checkpoint 1 Due
Thu, Nov 19 | Final Projects (maybe special topic)              | Checkpoint 2 Due               
Thu, Nov 21 | Final Projects (maybe special topic)              | Checkpoint 3 Due
Tue, Nov 26 | *Thanksgiving Recess*                             | Checkpoint 4 Due
Thu, Nov 28 | *Thanksgiving Recess*                             | 
Tue, Dec 03 | Final Projects                                    | Checkpoint 5 Due
Thu, Dec 05 | Final Project Presentations                       | Final Project Due (Fri, Dec 06, 11:59 PM)

[LN1]: ln/ln1.md.html
[LN2]: ln/ln2.md.html
[LN3]: ln/ln3.md.html
[LN4]: ln/ln4.md.html
[LN5]: ln/ln5.md.html
[LN6]: ln/ln6.md.html
[LN7]: ln/ln7.md.html
[LN8]: ln/ln8.md.html
[LN9]: ln/ln9.md.html

[HW1]: hw/HW1.agda.html
[HW2]: hw/HW2.agda.html
[HW3]: hw/HW3.agda.html
[HW4]: hw/HW4.agda.html
[HW5]: hw/HW5.agda.html
[HW6]: hw/HW6.agda.html
[HW7]: hw/HW7.agda.html
[HW8]: hw/HW8.agda.html
[HW9]: hw/HW9.agda.html
[HW10]: hw/HW10.agda.html

[HW1-DL]: hw/HW1.agda
[HW2-DL]: hw/HW2.agda
[HW3-DL]: hw/HW3.agda
[HW4-DL]: hw/HW4.agda
[HW5-DL]: hw/HW5.agda
[HW6-DL]: hw/HW6.agda
[HW7-DL]: hw/HW7.agda
[HW8-DL]: hw/HW8.agda
[HW9-DL]: hw/HW9.agda
[HW10-DL]: hw/HW10.agda

[IC3]: ic/IC3.agda
[IC4]: ic/IC4.agda
[IC5]: ic/IC5.agda
[IC6]: ic/IC6.agda
[IC7]: ic/IC7.agda
[IC8]: ic/IC8.agda
[IC9]: ic/IC9.agda
[IC10]: ic/IC10.agda
[IC11]: ic/IC11.agda
[IC12]: ic/IC12.agda

[IC3-SL]: ic/IC3-SL.agda.html
[IC4-SL]: ic/IC4-SL.agda.html
[IC5-SL]: ic/IC5-SL.agda.html
[IC6-SL]: ic/IC6-SL.agda.html
[IC7-SL]: ic/IC7-SL.agda.html
[IC8-SL]: ic/IC8-SL.agda.html
[IC9-SL]: ic/IC9-SL.agda.html
[IC10-SL]: ic/IC10-SL.agda.html
[IC11-SL]: ic/IC11-SL.agda.html
[IC12-SL]: ic/IC12-SL.agda.html