Unless otherwise stated, all homeworks are due at 11:59pm. Written homework should be submitted through Gradescope. Please notify the course staff if you have not already received an email to enroll in the relevant Gradescope instance.

In order to submit on Gradescope, your homework will need to be in PDF format. You are highly encouraged to typeset your solutions in LaTeX, and you will find appropriate templates for each assignment below. Your graders strongly prefer LaTeX-typeset solutions, as your work is much more likely to be clear and legible, as well as consistent with the formatting they expect to see. We recognize that certain types of answers, such as those that involve graphical figures or structured formatting, can be difficult or tedious to typeset. In those cases, the template will sometimes give an example in the comments that you are encouraged to emulate, but it is fine to scan a handwritten solution to include in your latex code as a graphic.

Labs should be submitted on the course Canvas website, under the relevant assignment. Upload a zip file named AndrewID-labN.zip, using your Andrew ID and the current lab number. The archive should contain your Why3 source and proofs along with any requested writing, following the instructions specified in the lab handout.

Relevant Links

assignment due date handout template
1: Prop it out 9/6 [pdf] [zip]
2: Program it out 9/13 [pdf] [zip]
3: Program with loops 9/20 [pdf] [zip]
4: Program with loops and arrays 9/28 [pdf] [zip]
5: Termination 10/7 [pdf] [zip]
6: Decision procedures and temporal properties 12/2 [pdf] [zip]


lab due date handout template
0: A first taste of Why3 9/21 [pdf] [mlw]
1: 4 Why you get to know Why3 10/9 [pdf] [mlw]
2: Implementing verified hash tables 11/2 [pdf] [mlw] [mlw]
3: Sheep SAT 11/13 [pdf] [mlw]
4 (Part 1): Unit propagation 12/4 (checkpoint on 11/27) [pdf] [mlw]
4 (Helper): Executing WhyML code [pdf] [zip]
4 (Part 2): Improvements 12/4 [pdf] [mlw]