A Practical Decision Procedure for Arithmetic with Function Symbols

Abstract

A practical procedure is presented for an extension of quantifier-free Presburger arithmetic that permits arbitrary unmterpreted predicate and function symbols This theory includes many of the formulas one tends to encounter in program venficatlon and is powerful enough to encode the semantics of array operators as well as MAX, MIN, and ABSVALUE An implementation of the procedure has proved to be of great value in a program verlficauon system developed at SRI for the United States Air Force