Course Information

Course Description

In this class, we look at a particularly intriguing example of how theory and practice can interact to create new knowledge and solve real-world problems. The focus of the class is verification techniques using first-order logic. We will discuss a number of different first-order theories, and look at algorithms for deciding certain kinds of formulas in these theories. The theories we will look at include the pure theory of equality with uninterprted functions, arithmetic (both real and integer), bit-vectors, and arrays. We will then look at methods of combining decision procedures and conclude with some applications to hardware and software verification.


Logic in Computer Science (G22-3033-002, Fall '03) or equivalent.


Wednesday 1:15pm-3:15pm in room 709 of 719 Broadway.

Mailing List

Everyone in the class should subscribe to the email list, as this is where important announcements will be sent. To subscribe, visit the following URL: