Checking validities and proofs with CVC and flea.

摘要

In automated reasoning, decision procedures are algorithms capable of reporting whether or not a formula is logically valid. Decision procedures are fundamental tools for formal verification. This thesis describes solutions to theoretical and engineering problems arising in the development of the CVC (“Cooperating Validity Checker”) decision procedure. CVC implements a framework that allows independent decision procedures for the quantifier-free consequences of different logical theories to be combined. Assuming certain properties of those decision procedures, the combination results in a sound and complete decision procedure for the quantifier-free consequences of the combined theory. There are currently decision procedures implemented for theories of arrays, linear real arithmetic, and inductive data types.; The thesis begins with an overview of the internals of CVC. Then CVC's array decision procedure is described. This is the first published procedure for its theory, which subsumes similar theories previously decided in the literature. Next, an approach is described for handling partial functions. The approach is based on a theorem reducing validity in a logic of partial functions to validity in classical logic. Then proof production in CVC is considered. CVC has the ability to produce a proof for every formula it reports to be valid. These proofs are produced in a proof meta-language based on the Edinburgh Logical Framework (LF). The proofs can be checked by a proof checker called flea. Several new language features are supported in flea which make it much easier to produce proofs from CVC. Also, flea implements new optimizations to the basic LF type-checking algorithm to be able to check the large proofs produced by CVC for large input formulas. Empirical results showing the benefits of the optimizations are presented. Finally, several uses of proofs beyond certifying correctness of CVC's results are described, including a technique which extracts information from proofs to feed back to CVC's propositional reasoning engine, the Chaff SAT solver, for improved performance.