Quantitative separation logic and programs with lists
DOI10.1007/S10817-010-9179-9zbMATH Open1207.03038OpenAlexW2055411475MaRDI QIDQ707740FDOQ707740
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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- BI as an assertion language for mutable data structures
- Arithmetic Strengthening for Shape Analysis
- An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
- Programs with Lists Are Counter Automata
- On the Almighty Wand
- Title not available (Why is that?)
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Foundations of Software Science and Computation Structures
- Title not available (Why is that?)
- A Logic-Based Framework for Reasoning about Composite Data Structures
- Computer Aided Verification
- Decision procedures for term algebras with integer constraints
- Locality Results for Certain Extensions of Theories with Bridging Functions
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
- Compositional invariant checking for overlaid and nested linked lists
- A complete decision procedure for linearly compositional separation logic with data constraints
- Quantitative Separation Logic and Programs with Lists
- Beyond Shapes: Lists with Ordered Data
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
Uses Software
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)
