| |
| |
| |
| Foundations | |
| |
| |
| |
| Propositional Logic | |
| |
| |
| |
| Syntax | |
| |
| |
| |
| Semantics | |
| |
| |
| |
| Satisfiability and Validity | |
| |
| |
| |
| Truth Tables | |
| |
| |
| |
| Semantic Arguments | |
| |
| |
| |
| Equivalence and Implication | |
| |
| |
| |
| Substitution | |
| |
| |
| |
| Normal Forms | |
| |
| |
| |
| Decision Procedures for Satisfiability | |
| |
| |
| |
| Simple Decision Procedures | |
| |
| |
| |
| Reconsidering the Truth-Table Method | |
| |
| |
| |
| Conversion to an Equisatisfiable Formula in CNF | |
| |
| |
| |
| The Resolution Procedure | |
| |
| |
| |
| DPLL | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| First-Order Logic | |
| |
| |
| |
| Syntax | |
| |
| |
| |
| Semantics | |
| |
| |
| |
| Satisfiability and Validity | |
| |
| |
| |
| Substitution | |
| |
| |
| |
| Safe Substitution | |
| |
| |
| |
| Schema Substitution | |
| |
| |
| |
| Normal Forms | |
| |
| |
| |
| Decidability and Complexity | |
| |
| |
| |
| Satisfiability as a Formal Language | |
| |
| |
| |
| Decidability | |
| |
| |
| |
| Complexity | |
| |
| |
| |
| Meta-Theorems of First-Order Logic | |
| |
| |
| |
| Simplifying the Language of FOL | |
| |
| |
| |
| Semantic Argument Proof Rules | |
| |
| |
| |
| Soundness and Completeness | |
| |
| |
| |
| Additional Theorems | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| First-Order Theories | |
| |
| |
| |
| First-Order Theories | |
| |
| |
| |
| Equality | |
| |
| |
| |
| Natural Numbers and Integers | |
| |
| |
| |
| Peano Arithmetic | |
| |
| |
| |
| Presburger Arithmetic | |
| |
| |
| |
| Theory of Integers | |
| |
| |
| |
| Rationals and Reals | |
| |
| |
| |
| Theory of Reals | |
| |
| |
| |
| Theory of Rationals | |
| |
| |
| |
| Recursive Data Structures | |
| |
| |
| |
| Arrays | |
| |
| |
| |
| Survey of Decidability and Complexity | |
| |
| |
| |
| Combination Theories | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| Induction | |
| |
| |
| |
| Stepwise Induction | |
| |
| |
| |
| Complete Induction | |
| |
| |
| |
| Well-Founded Induction | |
| |
| |
| |
| Structural Induction | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| Program Correctness: Mechanics | |
| |
| |
| |
| pi: A Simple Imperative Language | |
| |
| |
| |
| The Language | |
| |
| |
| |
| Program Annotations | |
| |
| |
| |
| Partial Correctness | |
| |
| |
| |
| Basic Paths: Loops | |
| |
| |
| |
| Basic Paths: Function Calls | |
| |
| |
| |
| Program States | |
| |
| |
| |
| Verification Conditions | |
| |
| |
| |
| P-Invariant and P-Inductive | |
| |
| |
| |
| Total Correctness | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| Program Correctness: Strategies | |
| |
| |
| |
| Developing Inductive Annotations | |
| |
| |
| |
| Basic Facts | |
| |
| |
| |
| The Precondition Method | |
| |
| |
| |
| A Strategy | |
| |
| |
| |
| Extended Example: QuickSort | |
| |
| |
| |
| Partial Correctness | |
| |
| |
| |
| Total Correctness | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| Algorithmic Reasoning | |
| |
| |
| |
| Quantified Linear Arithmetic | |
| |
| |
| |
| Quantifier Elimination | |
| |
| |
| |
| Quantifier Elimination | |
| |
| |
| |
| A Simplification | |
| |
| |
| |
| Quantifier Elimination over Integers | |
| |
| |
| |
| Augmented Theory of Integers | |
| |
| |
| |
| Cooper's Method | |
| |
| |
| |
| A Symmetric Elimination | |
| |
| |
| |
| Eliminating Blocks of Quantifiers | |
| |
| |
| |
| Solving Divides Constraints | |
| |
| |
| |
| Quantifier Elimination over Rationals | |
| |
| |
| |
| Ferrante and Rackoff's Method | |
| |
| |
| |
| Complexity | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| Quantifier-Free Linear Arithmetic | |
| |
| |
| |
| Decision Procedures for Quantifier-Free Fragments | |
| |
| |
| |
| Preliminary Concepts and Notation | |
| |
| |
| |
| Linear Programs | |
| |
| |
| |
| The Simplex Method | |
| |
| |
| |
| From M to M[subscript 0] | |
| |
| |
| |
| Vertex Traversal | |
| |
| |
| |
| Complexity | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| Quantifier-Free Equality and Data Structures | |
| |
| |
| |
| Theory of Equality | |
| |
| |
| |
| Congruence Closure Algorithm | |
| |
| |
| |
| Relations | |
| |
| |
| |
| Congruence Closure Algorithm | |
| |
| |
| |
| Congruence Closure with DAGs | |
| |
| |
| |
| Directed Acyclic Graphs | |
| |
| |
| |
| Basic Operations | |
| |
| |
| |
| Congruence Closure Algorithm | |
| |
| |
| |
| Decision Procedure for T[subscript E]-Satisfiability | |
| |
| |
| |
| Complexity | |
| |
| |
| |
| Recursive Data Structures | |
| |
| |
| |
| Arrays | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| Combining Decision Procedures | |
| |
| |
| |
| Combining Decision Procedures | |
| |
| |
| |
| Nelson-Oppen Method: Nondeterministic Version | |
| |
| |
| |
| Phase 1: Variable Abstraction | |
| |
| |
| |
| Phase 2: Guess and Check | |
| |
| |
| |
| Practical Efficiency | |
| |
| |
| |
| Nelson-Oppen Method: Deterministic Version | |
| |
| |
| |
| Convex Theories | |
| |
| |
| |
| Phase 2: Equality Propagation | |
| |
| |
| |
| Equality Propagation: Implementation | |
| |
| |
| |
| Correctness of the Nelson-Oppen Method | |
| |
| |
| |
| Complexity | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| Arrays | |
| |
| |
| |
| Arrays with Uninterpreted Indices | |
| |
| |
| |
| Array Property Fragment | |
| |
| |
| |
| Decision Procedure | |
| |
| |
| |
| Integer-Indexed Arrays | |
| |
| |
| |
| Array Property Fragment | |
| |
| |
| |
| Decision Procedure | |
| |
| |
| |
| Hashtables | |
| |
| |
| |
| Hashtable Property Fragment | |
| |
| |
| |
| Decision Procedure | |
| |
| |
| |
| Larger Fragments | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| Invariant Generation | |
| |
| |
| |
| Invariant Generation | |
| |
| |
| |
| Weakest Precondition and Strongest Postcondition | |
| |
| |
| |
| General Definitions of wp and sp | |
| |
| |
| |
| Static Analysis | |
| |
| |
| |
| Abstraction | |
| |
| |
| |
| Interval Analysis | |
| |
| |
| |
| Karr's Analysis | |
| |
| |
| |
| Standard Notation and Concepts | |
| |
| |
| |
| Summary | |
| |
| |
| Bibliographic Remarks | |
| |
| |
| Exercises | |
| |
| |
| |
| Further Reading | |
| |
| |
| References | |
| |
| |
| Index | |