Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fifteenth Annual IEEE Symposium on

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 Symposium on Logic in Computer Science (LICS 2000)},
    year =	 {2000},
    month =	 {June}, 
    pages =      {279--290},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski