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
EditorsAlbert Camilleri, Mandayam Srivas
PublisherSpringer Verlag
Pages187-201
Number of pages15
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)0302-9743
ISSN (Electronic)1611-3349

Other

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Validity checking for combinations of theories with equality'. Together they form a unique fingerprint.

Cite this