A practical integration of first-order reasoning and decision procedures

Abstract

We present a procedure for proving the validity of first-order formulas in the presence of decision procedures for an interpreted subset of the language. The procedure is designed to be practical: formulas can have large complex boolean structure, and include structure sharing in the form of let- expressions. The decision procedures are only required to decide the unsatisfiability of sets of literals. However, T-refuting substitutions are used whenever they can be computed; we show how this can be done for a theory of partial orders and equality. The procedure has been implemented as part of STeP, a tool for the formal verification of reactive systems. Although the procedure is incomplete, it eliminates the need for user interaction in the proof of many verification conditions.