Mechanized Verification with Sharing

Gregory Malecha, Greg Morrisett

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.

coq separation logic ynot

download slides publisher's link

@incollection{
  year={2010},
  isbn={978-3-642-14807-1},
  booktitle={Theoretical Aspects of Computing – ICTAC 2010},
  volume={6255},
  series={Lecture Notes in Computer Science},
  editor={Cavalcanti, Ana and Deharbe, David and Gaudel, Marie-Claude and Woodcock, Jim},
  doi={10.1007/978-3-642-14808-8_17},
  title={Mechanized Verification with Sharing},
  url={http://dx.doi.org/10.1007/978-3-642-14808-8_17},
  publisher={Springer Berlin Heidelberg},
  author={Malecha, Gregory and Morrisett, Greg},
  pages={245-259},
  language={English}
}