Accurate invariant checking for programs manipulating lists and arrays with infinite data

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 , 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 formulas, which is crucial in performing pre-post condition reasoning. Although this problem is undecidable in general for , 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 including known decidable logics. We implemented this procedure and shown its preciseness and its efficiency on a significant benchmark of formulas.