Treffer: Local reasoning for abstraction and sharing
Title:
Local reasoning for abstraction and sharing
Authors:
Contributors:
The Pennsylvania State University CiteSeerX Archives
Publisher Information:
ACM
Publication Year:
2009
Collection:
CiteSeerX
Subject Terms:
Categories and Subject Descriptors D.1.4 [Programming Techniques, Sequential Program- ming, D.2.2 [Software Engineering, Design Tools and Techniques—Modules and interfaces, D.2.4 [Software En- gineering, Software/Program Verification—Validation, Formal methods, Correctness proofs, D.3.3 [Programming Languages, Language Constructs and Features—Abstract data types, Constraints, F.3.1 [Logics and Meanings of Programs, Specifying and Verifying and Reasoning about Programs General Terms Languages, Reliability, Verification Keywords separation logic
Document Type:
Fachzeitschrift
text
File Description:
application/pdf
Language:
English
Relation:
Availability:
Rights:
Metadata may be used without restrictions as long as the oai identifier remains attached to it.
Accession Number:
edsbas.C4EDD789
Database:
BASE
Weitere Informationen
The local reasoning provided by Separation Logic has been proven to be a good tool for the verification of programs with complex pointer manipulation. However, some prob-lems arise when many structures share part of the heap since it becomes difficult to specify separately and it is even harder to preserve the abstractions that these structures pro-vide. In this article, we present a generalization of Separa-tion Logic which allows us to precisely specify complex ab-stract structures in the heap and the sharing relations among them. Moreover, we provide also a compositional proof the-ory which can be used to verify programs in a modular way, even when a complete separation of the structures cannot be ensured.