@inbook {IOPORT.06109367,
    author       = {Bouajjani, Ahmed and Dr\u{a}goi, Cezara and Enea, Constantin and Sighireanu, Mihaela},
    title        = {Accurate invariant checking for programs manipulating lists and arrays with infinite data.},
    year         = {2012},
    booktitle    = {Automated technology for verification and analysis. 10th international symposium, ATVA 2012, Thiruvananthapuram, India, October 3--6, 2012. Proceedings},
    isbn         = {978-3-642-33385-9},
    pages        = {167-182},
    publisher    = {Berlin: Springer},
    doi          = {10.1007/978-3-642-33386-6_14},
    abstract     = {Summary: We propose a logic-based framework for automated reasoning about sequential programs manipulating singly-linked lists and arrays with unbounded data. We introduce the logic $\text{SLAD}$, which allows combining shape constraints, written in a fragment of Separation Logic, with data and size constraints. We address the problem of checking the entailment between $\text{SLAD}$ formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for $\text{SLAD}$, we propose a sound and powerful procedure that is able to solve this problem for a large class of formulas, beyond the capabilities of existing techniques and tools. We prove that this procedure is complete, i.e., it is actually a decision procedure for this problem, for an important fragment of $\text{SLAD}$ including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas.},
    identifier   = {06109367},
}