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)

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)