\input zb-basic
\input zb-ioport
\iteman{io-port 06109367}
\itemau{Bouajjani, Ahmed; Dr\u{a}goi, Cezara; Enea, Constantin; Sighireanu, Mihaela}
\itemti{Accurate invariant checking for programs manipulating lists and arrays with infinite data.}
\itemso{Chakraborty, Supratik (ed.) et al., Automated technology for verification and analysis. 10th international symposium, ATVA 2012, Thiruvananthapuram, India, October 3--6, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-33385-9/pbk). Lecture Notes in Computer Science 7561, 167-182 (2012).}
\itemab
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.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-33386-6\_14}
\end