Speaker:    Natarajan Shankar
Title:  Little Engines of Proof

Verification aims to show that computer hardware and software designs
achieve their intended function.  The construction of a mathematical proof
is one method for debugging and verifying the correctness of complex
designs.  Proofs of this scale can be reliably constructed only through
the use of efficient automation.  In the absence of a single
sledgehammer for automating proofs, some quite modest decision
procedures are finding limited success.  These include propositional
satisfiability solvers, ground decision procedures for equality and
arithmetic, quantifier elimination procedures for integers and reals, and
abstraction techniques for finding finite approximations of problems over
infinite domains.  We describe some of these "little engines of proof" and
the challenge of building proofs that combine individual decision methods.

Work address:    SRI International Computer Science Laboratory,
   Menlo Park CA 94025 USA

Electronic Mail: shankar@csl.sri.com