Quantitative separation logic and programs with lists

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

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

decidability; separation logic; program verification; list structures; Presburger constraint

Mathematics Subject Classification ID

03B70: Logic in computer science

03B25: Decidability of theories and sets of sentences

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

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