@inproceedings{
    JunttilaDubrovin:LPAR2008,
    editor = "Cervesato, Iliano and Veith, Helmut and Voronkov, Andrei",
    author = "Junttila, Tommi and Dubrovin, Jori",
    publisher = "Springer",
    optmonth = "November 22--27",
    responsibleauthor = "Tommi Junttila",
    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 Artificial Intelligence",
    booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08)",
    optaddress = "Doha, Qatar",
    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.",
    volume = "5330",
    flags = "DC",
    year = "2008",
    keywords = "software verification, bounded model checking, satisfiability modulo theories, queues",
    impactfactor = "D3",
    pages = "290--304"
}