Publication: Mechanized Verification with Sharing
Loading...
Open/View Files
Date
2010
Published Version
Journal Title
Journal ISSN
Volume Title
Publisher
Springer Verlag
The Harvard community has made this article openly available. Please share how this access benefits you.
Citation
Malecha, Gregory Michael, and John Gregory Morrisett. 2010. Mechanized verification with sharing. In Theoretical Aspects of Computing - ICTAC 2010: Proceedings of the 7th International Colloquium: Natal, Brazil, 1-3 September, 2010, ed. Ana Cavalcanti, David Deharbe, Marie-Claude Gaudel, and Jim Woodcock, 245-259. Berlin: Springer-Verlag.
Abstract
We consider software verification of imperative programs by theorem proving in higher-order separation logic. Separation logic is quite effective for reasoning about tree-like data structures, but less so for data structures with more complex sharing patterns. This problem is compounded by some higher-order patterns, such as stateful iterators and visitors, where multiple clients need to share references into a data structure. We show how both styles of sharing can be achieved without sacrificing abstraction using mechanized reasoning about fractional permissions in Hoare Type Theory.
Description
Other Available Sources
Research Data
Keywords
Terms of Use
This article is made available under the terms and conditions applicable to Open Access Policy Articles (OAP), as set forth at Terms of Service