| This thesis concentrates on the development of decision procedures to tackle challenges met in the combination of model checking, abstract interpretation and deductive methods for verification of reactive systems.; Proof-obligations are here often formulated using operations from different theories. For parameterized programs and real-time systems, verification conditions also often include quantifiers, so ground reasoning is not enough; pure first-order reasoning is on the other hand outperformed by specialized constraint solvers, such as linear programming techniques. We aim at combining quantifier reasoning with decision procedures.; For this purpose this thesis presents decision procedures for quantifier-free logics which are combined into a general validity checker by maintaining constraints incrementally. This is extended to first-order reasoning using rigid E-unification procedures. We use a new congruence closure algorithm for the integration of decision procedures. One of its attractive features is that it can tightly integrate theories over co-recursive data types. We also show how the congruence closure algorithm is extended to support special relations.; An attractive feature of combining decision procedures within a congruence closure algorithm is a tight and therefore efficient integration. The approach is however essentially limited to theories that are solvable. In solvable theories all implied equalities can be summarized using substitutions.; The limitation naturally challenges this as a basis for combining decision procedures. By presenting a spectrum of decision procedures that can be integrated in the framework we give evidence for the wide scope of this approach: an extension of Fourier's algorithm for quantifier elimination of linear arithmetical expressions, which extracts implicitly implied equalities on the fly, tightly integrated with a partial decision procedure for non-linear arithmetic; decision procedures for both recursive and co-recursive data types, including subterm relations and a length measure for recursive data-types; an algorithm for deciding a class of equational constraints between non-fixed size bit-vectors; and algorithms for reasoning about constraints over queues (lists where elements can be added to the front and the back), including sub-queue, prefix, suffix relations and support for length measures.; The decision procedures have been used in STeP, the Stanford Temporal Prover, and we report on experience on verification examples. |
