Table of Contents | Slides and Extra Reading | Projects | Software Download |

By Daniel Kroening and Ofer Strichman | ||

(click to enlarge) |
A The authors introduce the basic terminology of satisfiability modulo theories and then, in separate chapters, study decision procedures for each of the following theories: - propositional logic
- equalities and uninterpreted functions
- linear arithmetic
- bit vectors
- arrays
- pointer logic
- quantified formulas.
They also study the problem of deciding combined theories and dedicate a chapter to modern techniques based on an interplay between a SAT solver and a decision procedure for the investigated theory. This textbook has been used to teach undergraduate and graduate courses at ETH Zurich, at the Technion, Haifa, and at the University of Oxford. Each chapter includes a detailed bibliography and exercises. Lecturers' slides and a C++ library for rapid prototyping of decision procedures are available from this website. The book is available at Springer and at Amazon. Springer also provides an online version. Clark Barrett has recently written a review of the book in JAR. (Errata) |