Skip to content

Calculus of Computation Decision Procedures with Applications to Verification

Best in textbook rentals since 2012!

ISBN-10: 3540741127

ISBN-13: 9783540741121

Edition: 2007

Authors: Aaron R. Bradley, Zohar Manna

List price: $79.99
Blue ribbon 30 day, 100% satisfaction guarantee!
what's this?
Rush Rewards U
Members Receive:
Carrot Coin icon
XP icon
You have reached 400 XP and carrot coins. That is the daily max!

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…    
Customers also bought

Book details

List price: $79.99
Copyright year: 2007
Publisher: Springer Berlin / Heidelberg
Publication date: 9/3/2007
Binding: Hardcover
Pages: 366
Size: 6.10" wide x 9.25" long x 0.41" tall
Weight: 1.034
Language: English

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