A Logic-Based Framework for Reasoning about Composite Data Structures

We define a logic, called CSL, for the specification of complex data structures, and we show its use in program verification. Our framework allows to handle programs with dynamic linked structures and arrays carrying unbounded data, as well as the composition of these structures. The formulas in CSL allow a limited form of alternation between existential and universal quantifiers and they can express (1) constraints on reachability between positions in the heap following some pointer fields, (2) linear constraints on the lengths of the lists and the indexes of the arrays, and (3) constraints on the values of the data attached to these positions. For data constraints, the logic CSL is parameterized by a first-order logic over the considered data domain. We prove that the satisfiability problem of CSL is decidable whenever the underlying data logic is decidable and that CSL is closed under the computation of the strongest post-condition in the considered class of programs.