@inproceedings{
    JunDub:LPAR08,
    editor = "Cervesato, Iliano and Veith, Helmut and Voronkov, Andrei",
    author = "Junttila, Tommi and Dubrovin, Jori",
    volume = "5330",
    publisher = "Springer",
    title = "Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking",
    url = "http://dx.doi.org/10.1007/978-3-540-89439-1_21",
    series = "Lecture Notes in Computer Science",
    booktitle = "Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 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.",
    responsibleauthor = "Junttila, Tommi",
    flags = "public copy",
    year = "2008",
    keywords = "software verification, bounded model checking, satisfiability modulo theories, queues",
    impactfactor = "D3",
    pages = "290--304"
}