Quantitative separation logic and programs with lists

DOI10.1007/S10817-010-9179-9MaRDI QIDQ707740zbMATH OpenOpenAlexFDO

Authors Marius Bozga, Radu Iosif, Swann Perarnau

Publication date 8 October 2010

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-010-9179-9

zbMATH Keywords

decidabilitylist structuresPresburger constraintprogram verificationseparation logic

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Review text

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.

Recommendations

• Quantitative Separation Logic and Programs with Lists
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Beyond Shapes: Lists with Ordered Data
• The effects of adding reachability predicates in propositional separation logic
• Separation logic with one quantified variable

Cites work

• A Logic-Based Framework for Reasoning about Composite Data Structures
• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
• Arithmetic Strengthening for Shape Analysis
• BI as an assertion language for mutable data structures
• Computer Aided Verification
• Decision procedures for term algebras with integer constraints
• Foundations of Software Science and Computation Structures
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• scientific article; zbMATH DE number 1796145 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• Locality Results for Certain Extensions of Theories with Bridging Functions
• On the Almighty Wand
• Programs with Lists Are Counter Automata

Cited in

(11)

• The effects of adding reachability predicates in propositional separation logic
• Automated mutual induction proof in separation logic
• A complete decision procedure for linearly compositional separation logic with data constraints
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• Quantitative Separation Logic and Programs with Lists
• Beyond Shapes: Lists with Ordered Data
• A complete axiomatisation for quantifier-free separation logic
• Expressive completeness of separation logic with two variables and no separating conjunction
• Compositional invariant checking for overlaid and nested linked lists
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Proving Termination of C Programs with Lists

Describes a project that uses

Uses Software

• FAST
• ARMC
• Aspic
• TREX

This page was built for publication: Quantitative separation logic and programs with lists

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q707740)