Integrating decision procedures for temporal verification.

摘要

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.