Compositional invariant checking for overlaid and nested linked lists

DOI10.1007/978-3-642-37036-6_9MaRDI QIDQ5326282zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cited in

(9)

• Compositional entailment checking for a fragment of separation logic
• Compositional entailment checking for a fragment of separation logic
• Separation logics and modalities: a survey
• Accurate invariant checking for programs manipulating lists and arrays with infinite data
• Decidability for entailments of symbolic heaps with arrays
• Decision Procedure for Entailment of Symbolic Heaps with Arrays
• Completeness of cyclic proofs for symbolic heaps with inductive definitions
• Restriction on cut rule in cyclic-proof system for symbolic heaps
• Deciding satisfiability for overlaid symbolic heaps

Describes a project that uses

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)