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.
Transition systems are a general and flexible technique for modeling the behavior of programs, but manually specifying a transition system for each program we'd like to reason about is tedious and potentially error-prone. Instead, we can use operational semantics to automatically map a program P to its corresponding transition system directly from P's syntax. In particular, we'll see how to do this for the small "Imp" language used to model imperative programs with unbounded loops.
Available on Gitlab cse505-26au: git clone https://gitlab.cs.washington.edu/cse505-26au/cse505-26au.git
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:
Read BP: Formal Proofs, the Fine Print and Side Effects - Toby Murray, Paul C. Van Oorschot. Write a 2-paragraph reflection or commentary. Submit to Gradescope. Optional readings (you may like these if you had Opinions about the previous reading):
Read Varieties of Static Analyzers: A Comparison with Astree - Patrick Cousot, Radhia Cousot, Jerome Feret, Antoine Mine, Laurent Mauborgne, David Monniaux, Xavier Rival. Write a 2-paragraph reflection or commentary. Submit your reflection on Gradescope This paper showcases the many features of a static analyzer, Astree, that make it successful in the aviation industry for formal verification. While this course is not about abstract interpretation, if you want to dive deeper into that kind of static analysis, you can check out CSE 503 (Software Engineering). I think the paper should still be relatively digestible. There may be a few terms that you find unfamiliar, so here's a short gloss: