Logic and Verification
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
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 email@example.com. Be sure to include
your NYU id.