Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking

Reference:

Tommi Junttila and Jori Dubrovin. Encoding queues in satisfiability modulo theories based bounded model checking. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), volume 5330 of Lecture Notes in Computer Science, pages 290–304. Springer, 2008.

Abstract:

Using a Satisfiability Modulo Theories (SMT) solver as the back-end in SAT-based software model checking allows common data types to be represented directly in the language of the solver. A problem is that many software systems involve first-in-first-out queues but current SMT solvers do not support the theory of queues. This paper studies how to encode queues in the context of SMT-based bounded model checking, using only widely supported theories such as linear arithmetic and uninterpreted functions. Various encodings with considerably different compactness and requirements for available theories are proposed. An experimental comparison of the relative efficiency of the encodings is given.

Keywords:

software verification, bounded model checking, satisfiability modulo theories, queues

Suggested BibTeX entry:

@inproceedings{JunDub:LPAR08,
    author = {Tommi Junttila and Jori Dubrovin},
    booktitle = {Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08)},
    editor = {Iliano Cervesato and Helmut Veith and Andrei Voronkov},
    pages = {290--304},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking},
    volume = {5330},
    year = {2008},
}