Manna

The Calculus of Computation

Aaron R. Bradley · Zohar Manna

The Calculus
of Computation
Decision Procedures
with Applications to Verification

With 60 Figures

123

Authors
Aaron R. Bradley
Zohar Manna
Gates Building, Room 481
Stanford University
Stanford, CA 94305
USA
arbrad@cs.stanford.edu
manna@cs.stanford.edu

Library of Congress Control Number: 2007932679

ACMComputing Classification (1998): B.8, D.1, D.2, E.1, F.1, F.3, F.4, G.2, I.1, I.2

ISBN 978-3-540-74112-1 Springer Berlin Heidelberg New York
This work is subject to copyright. All rights are reserved, whether the whole or part of the material
is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilm or in any otherway, and storage in data banks. Duplication of
this publication or parts thereof is permitted only under the provisions of the German Copyright Law
of September 9, 1965, in its current version, and permission for use must always be obtained from
Springer. Violations are liable for prosecution under the German Copyright Law.
Springer is a part of Springer Science+Business Media
springer.com
©Springer-Verlag Berlin Heidelberg 2007
The use of general descriptive names, registered names, trademarks, etc. in this publication does not
imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use.
Typesetting by the authors
Production: LE-TEX Jelonek, Schmidt & Vöckler GbR, LeipzigCover design: KünkelLopka Werbeagentur, Heidelberg
Printed on acid-free paper

45/3180/YL - 5 4 3 2 1 0

To my wife,
Sarah
A.R.B.

To my grandchildren,
Itai
Maya
Ori
Z.M.

Preface

Logic is the calculus of computation. Forty-five years ago, John McCarthy
predicted in A Basis for a Mathematical Theory of Computation that “the
relationship between computation and mathematical logicwill be as fruitful in
the next century as that between analysis and physics in the last”. The field of
computational logic emerged over the past few decades in partial fulfillment
of that vision. Focusing on producing efficient and powerful algorithms for
deciding the satisfiability of formulae in logical theories and fragments, it
continues to push the frontiers of general computer science.This book is about computational logic and its applications to program
verification. Program verification is the task of analyzing the correctness of a
program. It encompasses the formal specification of what a program should do
and the formal proof that the program meets this specification. The reasoning
power that computational logic offers revolutionized the field of verification.
Ongoing researchwill make verification standard practice in software and
hardware engineering in the next few decades. This acceptance into everyday
engineering cannot come too soon: software and hardware are becoming ever
more ubiquitous and thus ever more the source of failure.
We wrote this book with an undergraduate and beginning graduate audience in mind. However, any computer scientist or engineer whowould like to
enter the field of computational logic or apply its products should find this
book useful.
Content
The book has two parts. Part I, Foundations, presents first-order logic, induction, and program verification. The methods are general. For example, Chapter 2 presents a complete proof system for first-order logic, while Chapter 5
describes a relatively complete verification methodology.Part II, Algorithmic
Reasoning, focuses on specialized algorithms for reasoning about fragments of
first-order logic and for deducing facts about programs. Part II trades generality for decidability and efficiency.

VIII

Preface

The first three chapters of Part I introduce first-order logic. Chapters 1 and
2 begin our presentation with a review of propositional and predicate logic.
Much of...