Syllabus
This course covers theory, implementation, and applications of automated reasoning techniques, such as satisfiability solving, theorem proving, model checking, and abstract interpretation. Topics include concepts from mathematical logic and applications of automated reasoning to the design, construction, and analysis of software.
Prerequisites
The course assumes that you know how to program, that you have taken a course in discrete mathematics, and that you have some familiarity with programming language semantics. You can use any language you want for your course project. However, you need to be comfortable compiling, installing, and running code written in C, C++, and Java. The tools covered in the course are written in these languages, and most are released as source code. Programming problems in homework assignments are written in Racket.
Course Materials
The course will not use a textbook, relying instead on:
- Lecture materials prepared by the instructor
- Tutorials, book chapters, and survey papers
- Classic research papers
- More recent research papers and documentation for modern tools
See the course calendar and references for details.
Grading
Homework (75%). There will be three homework assignments, weighted equally. The assignments may ask you to solve conceptual problems, implement programming challenges, and use existing computer-aided tools.
Project (25%). You will also work in a team of 2-3 students on a mini research project that applies computer-aided reasoning to software; think of it as a small workshop paper. The goal is to apply an existing computer-aided tool to a new domain, or to create a tool that can automatically reason about programs in a new or existing language. The project will take 5 weeks, with proposals due at the midpoint of the course. A final report and demo of the project are due at the end of the course. The scores you receive on project milestones will be weighted as follows:
| Weight | Milestone |
|---|---|
| 5% | Project Proposal |
| 10% | Project Demo |
| 10% | Final Report |
Late Policy
Both project and homework assignments must be turned in by the due date and time. You may use up to 2 late days per assignment, but no credit will be given for submissions after the late period. Also, the staff will not discuss the homework problems with you after the due date. Unless otherwise noted, all assignments should be submitted via the course dropbox.
Regrade Policy
We will entertain questions about grades only for one week after they are posted in the course gradebook. Questions about grades should be written and submitted to the course staff via an direct message on the course discussion board.
Academic Integrity
The homework assignments should be completed with a partner. You may discuss the homework problems in detail with your partner and with the course staff. You may also discuss the problems at a high level with other students in the course, but you may not share solutions, diagrams, or code with others. You must cite any reference materials (other than the lecture slides and course readings) used to complete an assignment, including books, papers, web resources (Wikipedia, StackOverflow, etc.), any conversations with other students, and generative AI tools (e.g., Copilot, ChatGPT, etc.).
You may (and should) make use of existing tools, libraries, and frameworks in your course project. But the final product must also include substantial new work (ideas, code, experiments, etc.).
See the UW CSE academic integrity policy for further details.