I will introduce the new textbook, "The Calculus of Computation: Decision Procedures 
with Applications to Verification," that I wrote with Zohar Manna.  We wrote the textbook
for advanced undergraduate and beginning graduate students, as well as computer 
scientists who desire a detailed introduction to satisfiability decision procedures.  My 
purpose in discussing it at this seminar is to bring it to the attention of colleagues who 
might use it in their courses.

Part I of the book provides a classical presentation of first-order logic, theories, induction, 
and program verification.  Part II studies algorithmic reasoning, in particular satisfiability 
decision procedures and static analyses.  Associated with the book is a freely available 
verifying compiler, \href{http://theory.stanford.edu/~arbrad/pivc}{"PiVC"}, which supports 
verification exercises in the book.