Quantitative separation logic and programs with lists

DOI10.1007/s10817-010-9179-9zbMath1207.03038OpenAlexW2055411475MaRDI QIDQ707740

Radu Iosif, Swann Perarnau, Marius Bozga

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

decidabilityseparation logicprogram verificationlist structuresPresburger constraint

Mathematics Subject Classification ID

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

Related Items

Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction, Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic, Automated mutual induction proof in separation logic, A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints, Unnamed Item

Uses Software

• TREX
• ARMC
• Aspic
• FAST

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Decision procedures for term algebras with integer constraints
• A Logic-Based Framework for Reasoning about Composite Data Structures
• On the Almighty Wand
• Arithmetic Strengthening for Shape Analysis
• BI as an assertion language for mutable data structures
• Locality Results for Certain Extensions of Theories with Bridging Functions
• Computer Aided Verification
• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Programs with Lists Are Counter Automata
• Foundations of Software Science and Computation Structures