This class is taught in Spring 2008. The overall content is similar to previous year's class, but more structured and with a larger role of final projects. Here are some online resources for the class.

The topics will come from three cross-cutting themes of software analysis and verification:

• logic and automated reasoning (first order and higher order logic, decision procedures, first-order provers, interactive provers)
• reasoning about programs (relational semantics of programs, verification condition generation, abstract interpretation)
• systems and methodology (modular analysis and specification, constraint solving, bug finding, tool integration, examples of existing tools)

The course emphasizes independent work and will require substantial investment of time beyond lecture notes and exercises. Although it is designated as a master's course, interested PhD students are encouraged to attend and can obtain credit for it.

Here is the official page in the course catalog, with course schedule.