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
No takes yet. Share an insight, caveat, or question.
Robert E. Shostak (1979) studied this question.
Synapse has enriched one closely related paper. Consider it for comparative context: