Syllabus
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, 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 |
Late Policy
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.
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 email.
Academic Integrity
The homework assignments should be done individually. This means that you may discuss homework problems only with the course staff. You may not discuss either problems or solutions with current or past CSE 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.