Logic in Computer Science (LICS 2000)

Paper: A Decision Procedure for Term Algebras with Queues (at LICS 2000)

Authors: Tatiana Rybina Andrei Voronkov

Abstract

In software verification it is often required to prove statements about heterogeneous domains containing elements of various sorts, such as counters, stacks, lists, trees and queues. Any domain with counters, stacks, lists, and trees (but not queues) can be easily seen a special case of the term algebra, and hence a decision procedure for term algebras can be applied to decide the first-order theory of such a domain.We present a quantifier-elimination procedure for the first-order theory of term algebras extended with queues. The complete axiomatization and decidability of this theory can be immediately derived from the procedure.

BibTeX

  @InProceedings{RybinaVoronkov-ADecisionProceduref,
    author = 	 {Tatiana Rybina and Andrei Voronkov},
    title = 	 {A Decision Procedure for Term Algebras with Queues},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {279--290},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }