Assignment 3: Verifying Go programs

In this assignment you'll verify imperative programs written in Go. All your proofs should be carried out in the exercises repo (sys-verif-fa24-proofs). The various parts of the assignment are divided among files in src/sys_verif/assignment3; each part is independent.

Submit your work by running ./etc/prepare-submit and uploading hw.tar.gz to the Canvas assignment.

Part 1 is a tutorial and part 2 is a warmup. Part 5 has an open-ended component (you'll write almost the entire proof yourself). Please take this into account when planning how to work on the assignment.

The point values add up to 90, but the assignment will be weighted in your overall grade as specified in the syllabus.

Part 1: Introduction to program proofs

5 points

See Intro to program proofs

Part 2: Inferring specifications

25 points

See Inferring specifications.

Part 3: Verify factorial

10 points

See Factorial.

Part 4: Linked lists

15 points

See Linked lists.

Part 5: Queue using two stacks

35 points

See Queue.