Each homework guarantees a fixed part of your final grade if solved. There are more problems than needed to earn a perfect grade. In case an assignment turns out to be significantly more challenging than anticipated, at most 50% of its intended credit may be awarded to everybody regardless of completion.
Unless otherwise specified, follow UW CSE policy AI for Ideation and Refinement
The assignments were designed to be completed without use of LLMs (the "AI" defined in the department policy). However, you may find it helpful to use some in lieu of a search engine, for example to understand (infamously dense) error messages from Rocq or to locate a tactic that would perform the desired low-level proof step at a goal you are trying to prove.
As solutions to the homeworks are both in the training data of most LLMs and reachable through simple web-search tool calls, it would defeat the purpose of this class to ask an LLM for a solution to the stated problems. We already know it would find one, maybe even one that we wrote. It is your responsibility to make sure your prompts steer the slop machine away from regurgitating a solution, as prose or as code.
If you use any LLM-based tools, you must upload full transcripts of all class-related prompts and responses, regardless of whether the output ended up in your solution.
A 24-hour extension is applied automatically to every due date; you do not need to request it separately from submitting the assignment.
We generally do not grant exceptions directly, especially last-minute or after-the-fact requests. However, we will honor official academic accommodations.
We will assume you have a working POSIX-ish development enviornment (make, etc).
Workable options include Linux, Mac, WSL.
Most homework is completed in the Rocq proof assistant. Productive use of Rocq requires an "IDE", for incremental compilation. Recompiling from scratch after every change is preposterously slow.
C-c RET.
\ c l. Or nvim.
Alt + Right.
Finally, install Rocq if you have not done so already:
Test by creating test.v using your editor and running past Compute 1+1. in it.
Available on Gitlab cse505-26au: git clone https://gitlab.cs.washington.edu/cse505-26au/cse505-26au.git
Upload to HW1 Gradescope; Entry Code: G76ZWE
Read Reflections on Trusting Trust - Ken Thompson - 1984. Write a 2-paragraph reflection or commentary. Submit to Gradescope.
Available on Gitlab cse505-26au: git clone https://gitlab.cs.washington.edu/cse505-26au/cse505-26au.git
Upload to Gradescope
Resources:
induction in Rocq
Discussion of the most general modeling technique in this course, transition systems. It resolves some limitations of interpreters (for example, for modeling nonterminating code) at the cost of some framework weight. Induction and strengthening induction hypotheses continues to be very important with either technique.
Read Read Social Processes and Proofs of Theorems and Programs - Richard DeMillo, Richard Lipton, Alan Perlis. Write a 2-paragraph reflection or commentary. Submit to Gradescope.
Past offerings of CSE505
Available on Gitlab cse505-26au: Upload to Gradescope by Tuesday 5pm for feedback. Use "QUESTION:" in your submission to call our attention to what you would like feedback on - perhaps strengthened inductive invariants, or another creative aspect. Upload final solution by Thursday 5pm.
Resources:Homework 3 (due 5pm on Oct 29): transition systems and invariants.
git clone https://gitlab.cs.washington.edu/cse505-26au/cse505-26au.git