Quantitative Separation Logic and Programs with Lists

This paper presents an extension of a decidable fragment of Separation Logic for singly-linked lists, defined by Berdine et al. ( 2004 ). Our main extension consists in introducing atomic formulae of the form ls k ( x , y ) describing a list segment of length k , stretching from x to y , where k is...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2010-08, Vol.45 (2), p.131-156
Main Authors: Bozga, Marius, Iosif, Radu, Perarnau, Swann
Format: Article
Language:English
Subjects:
Arithmetic
Artificial Intelligence
Computer Science
Embedded Systems
Graphs
Lists
Logic
Logic in Computer Science
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Mathematical models
Segments
Separation
Stretching
Symbolic and Algebraic Manipulation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper presents an extension of a decidable fragment of Separation Logic for singly-linked lists, defined by Berdine et al. ( 2004 ). Our main extension consists in introducing atomic formulae of the form ls 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 may occur further inside Presburger constraints. We study the decidability of the full first-order logic combining unrestricted quantification of arithmetic and location variables. Although the full logic is found to be undecidable, validity of entailments between formulae with the quantifier prefix in the language is decidable. We provide here a model theoretic method, based on a parametric notion of shape graphs. We have implemented our decision technique, providing a fully automated framework for the verification of quantitative properties expressed as pre- and post-conditions on programs working on lists and integer counters.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-010-9179-9