By Daniel Kroening and Ofer Strichman
(click to enlarge)		1 Introduction and Basic Concepts    1.1 Two Approaches to Formal Reasoning    1.2 Basic Definitions    1.3 Normal Forms and Some of Their Properties    1.4 The Theoretical Point of View    1.5 Expressiveness vs. Decidability    1.6 Boolean Structure in Decision Problems    1.7 Problems    1.8 Glossary 2 Decision Procedures for Propositional Logic    2.1 Propositional Logic    2.2 SAT Solvers    2.3 Binary Decision Diagrams    2.4 Problems    2.5 Bibliographic Notes    2.6 Glossary 3 Equalities and Uninterpreted Functions    3.1 Introduction    3.2 Uninterpreted Functions    3.3 From Uninterpreted Functions to Equality Logic    3.4 Functional Consistency Is Not Enough    3.5 Two Examples of the Use of Uninterpreted Functions    3.6 Problems    3.7 Glossary 4 Decision Procedures for Equality Logic and Uninterpreted Functions    4.1 Congruence Closure    4.2 Basic Concepts    4.3 Simplifications of the Formula    4.4 A Graph-Based Reduction to Propositional Logic    4.5 Equalities and Small-Domain Instantiations    4.6 Ackermann's vs. Bryant's Reduction: Where Does It Matter?    4.7 Problems    4.8 Bibliographic Notes    4.9 Glossary 5 Linear Arithmetic    5.1 Introduction    5.2 The Simplex Algorithm    5.3 The Branch and Bound Method    5.4 Fourier-Motzkin Variable Elimination    5.5 The Omega Test    5.6 Preprocessing    5.7 Difference Logic    5.8 Problems    5.9 Bibliographic Notes    5.10 Glossary 6 Bit Vectors    6.1 Bit-Vector Arithmetic    6.2 Deciding Bit-Vector Arithmetic with Flattening    6.3 Incremental Bit Flattening    6.4 Using Solvers for Linear Arithmetic    6.5 Fixed-Point Arithmetic    6.6 Problems    6.7 Bibliographic Notes    6.8 Glossary 7 Arrays    7.1 Introduction    7.2 Arrays as Uninterpreted Functions    7.3 A Reduction Algorithm for Array Logic    7.4 Problems    7.5 Bibliographic Notes    7.6 Glossary 8 Pointer Logic    8.1 Introduction    8.2 A Simple Pointer Logic    8.3 Modeling Heap-Allocated Data Structures    8.4 A Decision Procedure    8.5 Rule-Based Decision Procedures    8.6 Problems    8.7 Bibliographic Notes    8.8 Glossary 9 Quantified Formulas    9.1 Introduction    9.2 Quantifier Elimination    9.3 Search-Based Algorithms for QBF    9.4 Problems    9.5 Bibliographic Notes    9.6 Glossary 10 Deciding a Combination of Theories    10.1 Introduction    10.2 Preliminaries    10.3 The Nelson-Oppen Combination Procedure    10.4 Problems    10.5 Bibliographic Notes    10.6 Glossary 11 Propositional Encodings    11.1 Overview    11.2 Lazy Encodings    11.3 Propositional Encodings with Proofs (Advanced)    11.4 Problems    11.5 Bibliographic Notes    11.6 Glossary A The SMT-LIB Initiative B A C++ Library for Developing Decision Procedures    B.1 Introduction    B.2 Graphs and Trees    B.3 Parsing    B.4 CNF and SAT    B.5 A Template for a Lazy Decision Procedure