Logic and Verification

Barrett, Clark

Graduate Division

Computer Science

Prerequisites: Ability to understand abstract mathematical concepts and proofs; ability to write reasonably sophisticated programs.

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 course begins with Boolean logic and functions. Boolean representations can be used to model a wide variety of interesting problems. We discuss methods such as binary decision diagrams (BDDs) and high-speed Boolean satisfiability (SAT) algorithms, and we will explore how these are used in practice.

We then move on to first-order logic. We discuss syntax and semantics of first-order logic and explore complexity and completeness results. We will then look at ways to use first-order logic in practical verification efforts and show how these techniques can be applied to hardware and software systems.

The web page for this course is now available under "Academics" from NYU Home. If you are not enrolled in the class but would like to access the web page, please send email to barrett@cs.nyu.edu. Be sure to include your NYU id.