A method ~s g~ven for dec~dlng formulas in combinations of unquantified first-order theories.Rather than couphng separate decision procedures for the contributing theories, the method makes use of a single, uniform procedure that minimizes the code needed to accommodate each additional theory.It ~s apphcable to theories whose semantics can be encoded within a certain class of purely equational canonical form theories that ~s closed under combination.Examples are given from the equational theories of integer and real anthmeUc, a subtheory of monadic set theory, the theory of cons, car, and cdr, and others.A discussion of the speed performance of the procedure and a proof of the theorem that underhes ~ts completeness are also g~ven.The procedure has been used extensively as the deductive core of a system for program specificaUon and verifcation.

Reliable computer systems must handle malfunctioning components that give conflicting information to different parts of the system.This situation can be expressed abstractly in terms of a group of generals of the Byzantine army camped with their troops around an enemy city.Communicating only by messenger, the generals must agree upon a common battle plan.However, one or more of them may be traitors who will try to confuse the others.The problem is to find an algorithm to ensure that the loyal generals will reach agreement.It is shown that, using only oral messages, this problem is solvable if and only if more than two-thirds of the generals are loyal; so a single traitor can confound two loyal generals.With unforgeable written messages, the problem is solvable for any number of generals and possible traitors.Applications of the solutions to reliable computer systems are then discussed.

V R Pratt has shown that the real and integer feastbdlty of sets of linear mequallUes of the form x _< y + c can be decided quickly by examining the loops m certain graphs Pratt's method is generahzed, first to real feaslbdlty of mequahues m two variables and arbitrary coefficients, and ultimately to real feaslbdlty of arbitrary sets of hnear mequahtles The method is well suited to apphcatlons m program verification KEY WORDS AND PHRASES theorem proving, decision procedures, program venficauon, linear programmmg CRCATEGORIES 3 15,369,521,532,541 lntroducttonProcedures for deciding whether a given set of linear inequalities has solutions often play an important role in deductive systems for program verification.Array bounds checks and tests on index variables are but two of the many common programming constructs that give rise to formulas involving inequalities.A number of approaches have been used to decide the feasibdity of sets of inequalities [3,8,9,16,22], ranging from goal-driven rewriting mechanisms [27] to the powerful simplex techniques [8] of linear programming.Some simple methods are well suited to the small, trivial problems that most often arise, but are insufficiently general.Full-scale simplex techniques, on the other hand, are general and fast for medium to large problems, but do not take advantage of the trivial structure of the small problems (revolving only a few variables and equations) encountered most frequently in program verification and related applications.The algorithm presented here retains the generality needed in the exceptional case, without sacrifice of speed and simplicity in the more typical small problem case.It builds on V. R. Pratt's observation [18, 20] that most of the inequalities that arise from verification conditions are of the form x _< y + c, where x and y are variables and c is a constant.Pratt showed that a conjunction of such inequalities can be decided quickly by examining the loops of a graph constructed from the inequalities of the conjunction.We generalize this approach, first to inequalities with no more

The problem addressed here concerns a set of isolated processors, some unknown subset of which may be faulty, that communicate only by means of two-party messages. Each nonfaulty processor has a private value of information that must be communicated to each other nonfaulty processor. Nonfaulty processors always communicate honestly, whereas faulty processors may lie. The problem is to devise an algorithm in which processors communicate their own values and relay values received from others that allows each nonfaulty processor to infer a value for each other processor. The value inferred for a nonfaulty processor must be that processor's private value, and the value inferred for a faulty one must be consistent with the corresponding value inferred by each other nonfaulty processor. It is shown that the problem is solvable for, and only for, n ≥ 3 m + 1, where m is the number of faulty processors and n is the total number. It is also shown that if faulty processors can refuse to pass on information but cannot falsely relay information, the problem is solvable for arbitrary n ≥ m ≥ 0. This weaker assumption can be approximated in practice using cryptographic methods.

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

This article presents an improved version of Bledsoe's SUP-INF method for proving theorems in a subclass of Presburger arithmetic The improved method is able to determine mvahdRy as well as vahdlty, and provides counterexamples for formulas determined to be mvahd A proof of correctness is given for the algorithms on which the method is based Implementation results are discussed, as is an apphcation to linear programming

We describe how to transform certain flowchart programs into equivalent explicit primitive recursive programs. The input/output correctness conditions for the transformed programs are more amenable to proof than the verification conditions for the corresponding flowchart programs. In particular, the transformed correctness conditions can often be verified automatically by the theorem prover developed by Boyer and Moore [1].