Decision Procedures -- An Algorithmic Point of View_Business

Table of Contents|Slides and Extra Reading|Projects|Software DownloadBy Daniel Kroening andOfer Strichman(click to enlarge)A decision procedure is an algorithm that, given a decision problem,terminates with a correct yes/no answer. Here, the authors focus ontheories that are expressive enough to model real problems, but are stilldecidable. Specifically, the book concentrates on decision procedures forfirst-order theories that are commonly used in automated verification andreasoning, theorem-proving, compiler optimization and operations research. The techniques described in the book draw from fields such as graph theoryand logic, and are routinely used in industry.The authors introduce the basic terminology of SAT, Satisfiability ModuloTheories (SMT) and the DPLL(T) framework. Then, in separate chapters, theystudy decision procedures for the following theories:equalities and uninterpreted functionslinear arithmeticbit vectors arrayspointer logicquantified formulas.The first edition of this book was adopted as a textbook in coursesworldwide. It was published in 2008 and the field now called SMT was thenin its infancy, without the standard terminology and canonic algorithms ithas now; this second edition reflects these changes. It brings forward theDPLL(T) framework. It also expands the SAT chapter with modern SATheuristics, and includes a new section about incremental satisfiability, andthe related Constraints Satisfaction Problem (CSP). The chapter aboutquantifiers was expanded with a new section about general quantificationusing E-matching and a section about Effectively Propositional Reasoning(EPR). The book also includes a new chapter on the application of SMT inindustrial software engineering and in computational biology, coauthored byNikolaj Bjørner and Leonardo de Moura, and Hillel Kugler, respectively.Each chapter includes a detailed bibliography and exercises. Lecturers' slides and a C++library for rapid prototyping of decision procedures are available fromthis website.The book is available atSpringerand at Amazon.Springer also provides an online version.Clark Barrett has written a review of the first edition of the book in JAR. Rosemary Monahanhas writtena reviewof the second edition of the book in FACJ. (Errata for the first edition,errata for the second edition)