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

decidabilityprogram verificationseparation logiclist structuresPresburger constraint

Mathematics Subject Classification ID

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

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

• 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?)
• 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
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Foundations of Software Science and Computation Structures
• Locality Results for Certain Extensions of Theories with Bridging Functions
• On the Almighty Wand
• Programs with Lists Are Counter Automata

Cited in

(11)

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

Describes a project that uses

Uses Software

• FAST
• Aspic
• ARMC
• 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)