Mechanized Verification with Sharing
MetadataShow full item record
CitationMalecha, 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.
AbstractWe 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.
Citable link to this pagehttp://nrs.harvard.edu/urn-3:HUL.InstRepos:10860121
- FAS Scholarly Articles