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.
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.
The course will not use a textbook, relying instead on
See the course calendar and references for details.
Homework (75%). There will be three homework assignments, weighted equally. The assignments may ask you to solve conceptual problems, programming problems, 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 |
Both project and homework assignments must be turned in by the due date and time in order to contribute to your grade. Assignments will not be accepted late. Unless otherwise noted, all assignments should be submitted via the course dropbox.
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 email.
You may discuss homework problems only with the TA and the instructor. You may not discuss either problems or solutions with current or past 507 students. You must cite any reference materials (other than the lecture slides) used to complete an assignment, including books, papers, and web resources (Wikipedia, StackOverflow, 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.