Mechanized Verication with Sharing
| Title: | Mechanized Verication with Sharing |
| Author: |
Malecha, Gregory Michael; Morrisett, John Gregory
Note: Order does not necessarily reflect citation order of authors. |
| Citation: | Malecha, Gregory Michael, and John Gregory Morrisett. 2010. Mechanized verication with sharing. In Theoretical Aspects of Computing - ICTAC 2010: Proceedings of the 7th International Colloquium: September 1-3, 2010, Natal, Brazil, ed. Ana Cavalcanti et al., 245-259. Berlin: Springer. |
| Full Text & Related Files: |
mechanized_verification.pdf (229.6Kb; PDF) 
|
| 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 reference 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. |
| Other Sources: | http://dl.acm.org/citation.cfm?id=1881855 |
| Terms of Use: | This article is made available under the terms and conditions applicable to Open Access Policy Articles, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#OAP |
| Citable link to this page: | http://nrs.harvard.edu/urn-3:HUL.InstRepos:9310887 |
This item appears in the following Collection(s)
-
FAS Scholarly Articles [5171]
Peer reviewed scholarly articles from the Faculty of Arts and Sciences of Harvard University
Contact administrator regarding this item (to report mistakes or request changes)
