Validity checking for combinations of theories with equality

Clark Barrett, David Dill, Jeremy Levitt

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationFormal Methods in Computer-Aided Design - 1st International Conference, FMCAD 1996, Proceedings
PublisherSpringer Verlag
Pages187-201
Number of pages15
Volume1166
ISBN (Print)3540619372, 9783540619376
DOIs
StatePublished - 1996
Event1st International Conference on Formal Methods in Computer-Aided Design, FMCAD 1996 - Palo Alto, United States
Duration: Nov 6 1996Nov 8 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1166
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other1st International Conference on Formal Methods in Computer-Aided Design, FMCAD 1996
CountryUnited States
CityPalo Alto
Period11/6/9611/8/96

    Fingerprint

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Barrett, C., Dill, D., & Levitt, J. (1996). Validity checking for combinations of theories with equality. In Formal Methods in Computer-Aided Design - 1st International Conference, FMCAD 1996, Proceedings (Vol. 1166, pp. 187-201). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1166). Springer Verlag. https://doi.org/10.1007/BFb0031808