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

Decision Procedures
Equality
Essential Component
Rewriting
Efficient Implementation
Congruence
Linear Inequalities
Sharing
Closure
Hardware
Heuristics
Logic
Experiment
Experiments

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

Validity checking for combinations of theories with equality. / Barrett, Clark; Dill, David; Levitt, Jeremy.

Formal Methods in Computer-Aided Design - 1st International Conference, FMCAD 1996, Proceedings. Vol. 1166 Springer Verlag, 1996. p. 187-201 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1166).

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

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, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1166, Springer Verlag, pp. 187-201, 1st International Conference on Formal Methods in Computer-Aided Design, FMCAD 1996, Palo Alto, United States, 11/6/96. https://doi.org/10.1007/BFb0031808
Barrett C, Dill D, Levitt J. Validity checking for combinations of theories with equality. In Formal Methods in Computer-Aided Design - 1st International Conference, FMCAD 1996, Proceedings. Vol. 1166. Springer Verlag. 1996. p. 187-201. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/BFb0031808
Barrett, Clark ; Dill, David ; Levitt, Jeremy. / Validity checking for combinations of theories with equality. Formal Methods in Computer-Aided Design - 1st International Conference, FMCAD 1996, Proceedings. Vol. 1166 Springer Verlag, 1996. pp. 187-201 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@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",
year = "1996",
doi = "10.1007/BFb0031808",
language = "English (US)",
isbn = "3540619372",
volume = "1166",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "187--201",
booktitle = "Formal Methods in Computer-Aided Design - 1st International Conference, FMCAD 1996, Proceedings",

}

TY - GEN

T1 - Validity checking for combinations of theories with equality

AU - Barrett, Clark

AU - Dill, David

AU - Levitt, Jeremy

PY - 1996

Y1 - 1996

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84957633777&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84957633777&partnerID=8YFLogxK

U2 - 10.1007/BFb0031808

DO - 10.1007/BFb0031808

M3 - Conference contribution

SN - 3540619372

SN - 9783540619376

VL - 1166

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 187

EP - 201

BT - Formal Methods in Computer-Aided Design - 1st International Conference, FMCAD 1996, Proceedings

PB - Springer Verlag

ER -