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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aydemir, B.E., Bohannon, A., Fairbairn, M., et al.: Mechanized Metatheory for the Masses: The PoplMark Challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50–65. Springer, Heidelberg (2005)
Bierhoff, K.: Iterator specification with typestates. In: SAVCBS 2006, pp. 79–82. ACM, New York (2006)
Bornat, R., Calcagno, C., OHearn, P.: Local reasoning, separation and aliasing. In: Proceedings of SPACE, vol. 4 (2004)
Chlipala, A., et al.: Effective interactive proofs for higher-order imperative programs. In: ICFP 2009, pp. 79–90. ACM, New York (2009)
Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA 1998, pp. 48–64. ACM, New York (1998)
Haack, C., Hurlin, C.: Separation Logic Contracts for a Java-Like Language with Fork/Join. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 199–215. Springer, Heidelberg (2008)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Boyland, J.: Checking Interference with Fractional Permissions, vol. 2694 (2003)
Jonas, B.J.: Specification and validation of data structures using separation logic. Master’s thesis, Technical University of Denmark (2010)
Kim, T., Bierhoff, K., Aldrich, J., Kang, S.: Typestate protocol specification in JML. In: SAVCBS 2009. ACM, New York (2009)
Krishnaswami, N.R.: Reasoning about iterators with separation logic. In: SAVCBS 2006, pp. 83–86. ACM, New York (2006)
Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: POPL 2010 (January 2010)
De Moura, L., Bjrner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory. In: ICFP 2006. ACM, New York (2006)
O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theoretical Computer Science 375(1-3), 271–307 (2007)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Symposium on Logic in Computer Science, LICS 2002 (2002)
Sexton, A., Thielecke, H.: Reasoning about B+ Trees with Operational Semantics and Separation Logic. Electronic Notes in Theoretical Computer Science 218, 355–369 (2008)
Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008)
Weide, B.W., et al.: Design and Specification of Iterators Using the Swapping Paradigm. IEEE Trans. Softw. Eng. 20(8), 631–643 (1994)
Weide, B.W.: SAVCBS 2006 challenge: specification of iterators. In: SAVCBS 2006, pp. 75–77. ACM, New York (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Malecha, G., Morrisett, G. (2010). Mechanized Verification with Sharing. In: Cavalcanti, A., Deharbe, D., Gaudel, MC., Woodcock, J. (eds) Theoretical Aspects of Computing – ICTAC 2010. ICTAC 2010. Lecture Notes in Computer Science, vol 6255. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14808-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-14808-8_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14807-1
Online ISBN: 978-3-642-14808-8
eBook Packages: Computer ScienceComputer Science (R0)