Malecha, Gregory MichaelMorrisett, Greg Gregory2013-07-052010Malecha, 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.978-3-642-14807-1http://nrs.harvard.edu/urn-3:HUL.InstRepos:10860121We 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.en-USConference Paper2013-06-26G. Malecha and G. Morrisett2013-07-0510.1007/978-3-642-14808-8_17