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 Autolab.
|1: Prop it out||9/7||[pdf]||[zip]|
|2: Program it out||9/14||[pdf]||[zip]|
|3: Program with loops||9/21||[pdf]||[zip]|
|4: Program with arrays||10/5||[pdf]||[zip]|
|5: Termination and DPLL||10/12||[pdf]||[zip]|
|7: Temporal properties and model checking||11/2||[pdf]||[zip]|
|0: A first taste of Why3||9/14||[pdf]||[mlw]|
|1: 4 Why we get to know Why3||10/6||[pdf]||[mlw]|
|2: Correct data structure invariants||10/23 (checkin), 10/31||[pdf]||[mlw1][mlw2]|
|3: Sheep SAT|
|4: DPLLesque SAT with unit propaganda|
|5: SPINning model checking with CTL|