Validity checking for combinations of theories with equality

Abstract. An essential component in many verication methods is a fast decision procedure for validating logical expressions. This paper presents the algorithm used in the Stanford Validity Checker (SVC) which has been used to aid several realistic hardware verication ef-forts. The logic for this decision procedure includes Boolean and un-interpreted functions and linear arithmetic. We have also successfully incorporated other interpreted functions, such as array operations and linear inequalities. The primary techniques which allow a complete and ecient implementation are expression sharing, heuristic rewriting, and congruence closure with interpreted functions. We discuss these tech-niques and present the results of initial experiments in which SVC is used as a decision procedure in PVS, resulting in dramatic speed-ups.