Unless otherwise stated, all homeworks are due at 11:59pm. Written homework should be submitted through Gradescope.

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 1/23 [pdf] [zip]
2: Program it out 2/4 [pdf] [zip]
3: Program with loops and arrays 2/23 [pdf] [zip]
4: Procedures: Imperative & otherwise 4/5 [pdf] [zip]
5: Linear Temporal Logic 4/17 [pdf] [zip]
6: Branching-Time Properties (extra credit) 5/1 [pdf] [zip]


lab due date handout template
0: A first taste of Why3 1/30 [pdf] [mlw]
1: 4 Why you get to know Why3 2/18 [pdf] [mlw]
2: Implementing verified hash tables 3/10 [pdf] [mlw]
3: Simple SAT 4/2 [pdf] [mlw]
4: Unit propagation 5/1 (checkpoint on 4/20) [pdf] [mlw]
Lab 4 Addendum: Compiling & running your solver [pdf] [zip]