Quantitative separation logic and programs with lists (Q707740)

An extension of a decidable fragment of Separation Logic for singly-linked lists is presented. The main extension consists in introducing atomic formulae of the form \(ks^k(x,y)\) describing a list segment of length \(k\), stretching from \(x\) to \(y\), where \(k\) is a logical variable interpreted over positive natural numbers, that occur further inside Presburger constraints. The decidability of the full first-order logic combining unrestricted quantification of arithmetic and location variables is studied. Although the full logic is undecidable, validity of entailments between formulae with the quantifier prefix in the language \(\exists^*\{\exists_{\mathbb N}, \forall_{\mathbb N}\}^*\) is decidable. The decision technique, providing a fully automated framework for the verification of quantitative properties expressed as pre- and post- conditions on programs working lists and integer counters, is implemented.