@inproceedings{3ccf4850dc264707a265f1f0afeae6bd,
title = "Validity checking for combinations of theories with equality",
abstract = "An essential component in many verification 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 verification efforts. 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 efficient implementation are expression sharing, heuristic rewriting, and congruence closure with interpreted functions. We discuss these techniques and present the results of initial experiments in which SVC is used as a decision procedure in PVS, resulting in dramatic speed-ups.",
author = "Clark Barrett and David Dill and Jeremy Levitt",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1996.; 1st International Conference on Formal Methods in Computer-Aided Design, FMCAD 1996 ; Conference date: 06-11-1996 Through 08-11-1996",
year = "1996",
doi = "10.1007/BFb0031808",
language = "English (US)",
isbn = "3540619372",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "187--201",
editor = "Albert Camilleri and Mandayam Srivas",
booktitle = "Formal Methods in Computer-Aided Design - 1st International Conference, FMCAD 1996, Proceedings",
}