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.
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: