Compositional invariant checking for overlaid and nested linked lists

DOI10.1007/978-3-642-37036-6_9zbMATH Open1381.68051OpenAlexW1506554338MaRDI QIDQ5326282FDOQ5326282

Authors: Constantin Enea, Vlad Saveluc, Mihaela Sighireanu 

Publication date: 5 August 2013

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-37036-6_9

Recommendations

• Compositional entailment checking for a fragment of separation logic
• Compositional entailment checking for a fragment of separation logic
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Accurate invariant checking for programs manipulating lists and arrays with infinite data
• Quantitative separation logic and programs with lists

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cited In (8)

• Title not available (Why is that?)
• Separation logics and modalities: a survey
• Decision Procedure for Entailment of Symbolic Heaps with Arrays
• Restriction on cut rule in cyclic-proof system for symbolic heaps
• Accurate invariant checking for programs manipulating lists and arrays with infinite data
• Compositional entailment checking for a fragment of separation logic
• Compositional entailment checking for a fragment of separation logic
• Completeness of cyclic proofs for symbolic heaps with inductive definitions

Uses Software

• VeriFast

This page was built for publication: Compositional invariant checking for overlaid and nested linked lists

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5326282)