Paper: Deconstructing Shostak (at LICS 2001)

Authors: Harald Rueß Natarajan Shankar

Abstract

Decision procedures for equality in a combination of theories are at the core of a number of verification systems. Shostak's 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 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.

BibTeX

  @InProceedings{RueShankar-DeconstructingShost,
    author = 	 {Harald Rueß and Natarajan Shankar},
    title = 	 {Deconstructing Shostak},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001)},
    year =	 {2001},
    month =	 {June}, 
    pages =      {19--28},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }