Local reasoning for global invariants. II: Dynamic boundaries

DOI10.1145/2485981MaRDI QIDQ5395717zbMATH OpenOpenAlexFDO

Authors Anindya Banerjee, David A. Naumann

Publication date 17 February 2014

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2485981

zbMATH Keywords

data abstractiondata invariantsheap separationinformation hidingmodularityresource protection

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Dynamic boundaries: information hiding by second order framing with first order assertions
• Local reasoning for global invariants. I: Region logic
• scientific article; zbMATH DE number 2087445
• Separation and information hiding
• A step-indexed Kripke model of hidden state

Cited in

(9)

• Unifying separation logic and region logic to allow interoperability
• Verified software units
• Dynamic boundaries: information hiding by second order framing with first order assertions
• Axiomization of passage from “local” structure to “global” object
• p‐Version interface elements in global/local analysis
• A step-indexed Kripke model of hidden state
• A first-order logic with frames
• Local reasoning for global invariants. I: Region logic
• The concept of class invariant in object-oriented programming

Describes a project that uses

Uses Software

• Spec#
• Boogie
• KRAKATOA
• jStar
• VCC

This page was built for publication: Local reasoning for global invariants. II: Dynamic boundaries

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