Local Reasoning for Global Invariants, Part II

DOI10.1145/2485981zbMath1281.68153OpenAlexW2100466897MaRDI QIDQ5395717

David A. Naumann, Anindya Banerjee

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

modularityinformation hidingdata abstractionresource protectiondata invariantsheap separation

Mathematics Subject Classification ID

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

Related Items (3)

A First-Order Logic with Frames ⋮ Verified software units ⋮ Unifying separation logic and region logic to allow interoperability

Uses Software

• KRAKATOA
• Spec#
• VCC
• Boogie
• jStar

This page was built for publication: Local Reasoning for Global Invariants, Part II