Title: Verifying the Composite pattern using separation logic
Authors: Jacobs, Bart ×
Smans, Jan
Piessens, Frank #
Issue Date: 9-Nov-2008
Conference: Workshop on Specification and Verification of Component-Based Systems, Challenge Problem Track edition:7 location:Atlanta, GA, USA date:9-10 November 2008
Abstract: Often, a module developer wishes to expose a graph of objects to client code, allowing client code to access the graph through any node directly, while maintaining hidden consistency conditions over the graph. In this note, we describe how to specify and verify such code using separation logic, using as an example a binary tree structure where each node keeps a count of its descendant nodes. The idea is to describe the tree structure as the separate conjunction of the focus node’s subtree and the focus node’s context. The description can be rewritten to use any other node as the focus node at any time. This enables an elegant modular proof of the tree implementation
on the one hand, and client code on the other hand.
We describe how we verified an example program using the
VeriFast program verifier prototype.
Publication status: published
KU Leuven publication type: IMa
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
composite.pdfWorkshop Paper Published 113KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.