Deconstructing Shostak

Decision procedures for equality in a combination of theories are at the core of a number of verification systems. R.E. Shostak's (J. of the ACM, vol. 31, no. 1, pp. 1-12, 1984) decision procedure for equality in the combination of solvable and canonizable theories has been around for nearly tw...

Full description

Saved in:
Bibliographic Details
Main Authors: Ruess, H., Shankar, N.
Format: Conference Proceeding
Language:English
Subjects:
Arithmetic
Computer science
Constraint theory
Contracts
Decision feedback equalizers
Equations
Laboratories
NASA
Partitioning algorithms
Static VAr compensators
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Decision procedures for equality in a combination of theories are at the core of a number of verification systems. R.E. Shostak's (J. of the ACM, vol. 31, no. 1, pp. 1-12, 1984) decision procedure for equality in the combination of solvable and canonizable theories has been around for nearly two decades. Variations of this decision procedure have been implemented in a number of specification and verification systems, including STP, EHDM, PVS, STeP and SVC. The algorithm is quite subtle and a correctness argument for it has remained elusive. Shostak's algorithm and all previously published variants of it yield incomplete decision procedures. We describe a variant of Shostak's algorithm, along with proofs of termination, soundness and completeness.
ISSN:1043-6871
2575-5528
DOI:10.1109/LICS.2001.932479