Calculus of computation : decision procedures with applications to verification / Aaron R. Bradley, Zohar Manna

Includes bibliographical references (p.[351]-355) and index.

Foundations Propositional Logicp. 3 Syntaxp. 4 Semanticsp. 6 Satisfiability and Validityp. 8 Truth Tablesp. 9 Semantic Argumentsp. 10 Equivalence and Implicationp. 14 Substitutionp. 16 Normal Formsp. 18 Decision Procedures for Satisfiabilityp. 21 Simple Decision Proceduresp. 21 Reconsidering the Truth-Table Methodp. 22 Conversion to an Equisatisfiable Formula in CNFp. 24 The Resolution Procedurep. 27 DPLLp. 28 Summaryp. 31 Bibliographic Remarksp. 32 Exercisesp. 32 First-Order Logicp. 35 Syntaxp. 35 Semanticsp. 39 Satisfiability and Validityp. 42 Substitutionp. 45 Safe Substitutionp. 47 Schema Substitutionp. 48 Normal Formsp. 51 Decidability and Complexityp. 53 Satisfiability as a Formal Languagep. 53 Decidabilityp. 54 Complexityp. 54 Meta-Theorems of First-Order Logicp. 56 Simplifying the Language of FOLp. 57 Semantic Argument Proof Rulesp. 58 Soundness and Completenessp. 58 Additional Theoremsp. 61 Summaryp. 66 Bibliographic Remarksp. 67 Exercisesp. 67 First-Order Theoriesp. 69 First-Order Theoriesp. 69 Equalityp. 71 Natural Numbers and Integersp. 73 Peano Arithmeticp. 73 Presburger Arithmeticp. 75 Theory of Integersp. 76 Rationals and Realsp. 79 Theory of Realsp. 80 Theory of Rationalsp. 82 Recursive Data Structuresp. 84 Arraysp. 87 Survey of Decidability and Complexityp. 90 Combination Theoriesp. 91 Summaryp. 92 Bibliographic Remarksp. 93 Exercisesp. 93 Inductionp. 95 Stepwise Inductionp. 95 Complete Inductionp. 99 Well-Founded Inductionp. 102 Structural Inductionp. 108 Summaryp. 110 Bibliographic Remarksp. 111 Exercisesp. 111 Program Correctness: Mechanicsp. 113 pi: A Simple Imperative Languagep. 114 The Languagep. 115 Program Annotationsp. 118 Partial Correctnessp. 123 Basic Paths: Loopsp. 125 Basic Paths: Function Callsp. 131 Program Statesp. 135 Verification Conditionsp. 136 P-Invariant and P-Inductivep. 142 Total Correctnessp. 143 Summaryp. 149 Bibliographic Remarksp. 150 Exercisesp. 151 Program Correctness: Strategiesp. 153 Developing Inductive Annotationsp. 153 Basic Factsp. 154 The Precondition Methodp. 156 A Strategyp. 162 Extended Example: QuickSortp. 164 Partial Correctnessp. 167 Total Correctnessp. 171 Summaryp. 172 Bibliographic Remarksp. 173 Exercisesp. 173 Algorithmic Reasoning Quantified Linear Arithmeticp. 183 Quantifier Eliminationp. 184 Quantifier Eliminationp. 184 A Simplificationp. 185 Quantifier Elimination over Integersp. 185 Augmented Theory of Integersp. 185 Cooper's Methodp. 187 A Symmetric Eliminationp. 194 Eliminating Blocks of Quantifiersp. 195 Solving Divides Constraintsp. 196 Quantifier Elimination over Rationalsp. 200 Ferrante and Rackoff's Methodp. 200 Complexityp. 204 Summaryp. 204 Bibliographic Remarksp. 205 Exercisesp. 205 Quantifier-Free Linear Arithmeticp. 207 Decision Procedures for Quantifier-Free Fragmentsp. 207 Preliminary Concepts and Notationp. 209 Linear Programsp. 213 The Simplex Methodp. 218 From M to M[subscript 0]p. 219 Vertex Traversalp. 223 Complexityp. 237 Summaryp. 237 Bibliographic Remarksp. 238 Exercisesp. 238 Quantifier-Free Equality and Data Structuresp. 241 Theory of Equalityp. 242 Congruence Closure Algorithmp. 244 Relationsp. 245 Congruence Closure Algorithmp. 247 Congruence Closure with DAGsp. 251 Directed Acyclic Graphsp. 251 Basic Operationsp. 254 Congruence Closure Algorithmp. 255 Decision Procedure for T[subscript E]-Satisfiabilityp. 256 Complexityp. 258 Recursive Data Structuresp. 259 Arraysp. 263 Summaryp. 265 Bibliographic Remarksp. 266 Exercisesp. 267 Combining Decision Proceduresp. 269 Combining Decision Proceduresp. 269 Nelson-Oppen Method: Nondeterministic Versionp. 271 Phase 1: Variable Abstractionp. 271 Phase 2: Guess and Checkp. 273 Practical Efficiencyp. 274 Nelson-Oppen Method: Deterministic Versionp. 276 Convex Theoriesp. 276 Phase 2: Equality Propagationp. 278 Equality Propagation: Implementationp. 282 Correctness of the Nelson-Oppen Methodp. 283 Complexityp. 287 Summaryp. 288 Bibliographic Remarksp. 288 Exercisesp. 288 Arraysp. 291 Arrays with Uninterpreted Indicesp. 292 Array Property Fragmentp. 292 Decision Procedurep. 294 Integer-Indexed Arraysp. 299 Array Property Fragmentp. 300 Decision Procedurep. 301 Hashtablesp. 304 Hashtable Property Fragmentp. 305 Decision Procedurep. 306 Larger Fragmentsp. 308 Summaryp. 309 Bibliographic Remarksp. 310 Exercisesp. 310 Invariant Generationp. 311 Invariant Generationp. 311 Weakest Precondition and Strongest Postconditionp. 312 General Definitions of wp and spp. 315 Static Analysisp. 316 Abstractionp. 319 Interval Analysisp. 325 Karr's Analysisp. 333 Standard Notation and Conceptsp. 341 Summaryp. 344 Bibliographic Remarksp. 345 Exercisesp. 345 Further Readingp. 347 Referencesp. 351 Indexp. 357 Table of Contents provided by Ingram. All Rights Reserved.

Computational logic is a fast-growing field with applications in artificial intelligence, constraint solving, and the design and verification of software and hardware systems. Written with graduate and advanced undergraduate students in mind, this textbook introduces computational logic from the foundations of first-order logic to state-of-the-art decision procedures for arithmetic, data structures, and combination theories. This textbook also presents a logical approach to engineering correct software. The increasing ubiquity of computers makes implementing correct systems more important than ever. Verification exercises develop the reader's facility in specifying and verifying software using logic. The treatment of verification concludes with an introduction to the static analysis of software, an important component of modern verification systems. For readers interested in learning more about computational logic, decision procedures, verification, and other areas of formal methods, the final chapter outlines courses of further study.

1