Abstract

Automated reasoning is a fundamental technology of increasing practical importance. The expressiveness of logics enable problems from a very wide range of practical applications to be reduced to logical problems. Dramatic improvements in implementation techniques in the past decade (e.g., for SAT solvers) have enabled more and more of the resulting logical problems to be solved efficiently. CVC ("a Cooperating Validity Checker") is a high-performance automated reasoning tool under development at Stanford ( http://verify.stanford.edu/CVC/). It implements a variant of the Nelson-Oppen method for combining satisfiability procedures. The current implementation has satisfiability procedures for theories of extensional arrays, linear real arithmetic, and inductive data types. CVC is a large (140kloc in C++) and complex piece of software. To increase confidence in its results, it has the ability to produce proofs of the formulas it claims are valid. The proofs are represented in a variant of the LF type theory, which has emerged as a popular meta-language for applications like proof-carrying code and proof-carrying authentication. For large valid formulas, CVC may produce very large proofs. These proofs are beyond the capacity of the standard LF proof-checking algorithm. The flea proof checker incorporates several new optimizations that enable these large proofs to be checked.
This talk highlights some of the theoretical and engineering problems solved in developing CVC and flea.