Abstract
We present an Isabelle/HOL library with a generic type class implementation of separation algebra, develop basic separation logic concepts on top of it, and implement generic automated tactic support that can be used directly for any instantiation of the library. We show that the library is usable by multiple example instantiations that include structures such as a heap or virtual memory, and report on our experience using it in operating systems verification.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bengtson, J., Jensen, J., Sieczkowski, F., Birkedal, L.: Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 22–38. Springer, Heidelberg (2011)
Calcagno, C., O’Hearn, P.W., Yang, H.: Local Action and Abstract Separation Logic. In: Proc. 22nd LICS, pp. 366–378. IEEE (2007)
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal Verification of an OS Kernel. In: 22nd SOSP, pp. 207–220. ACM (October 2009)
Klein, G., Kolanski, R., Boyton, A.: Separation Algebra. Archive of Formal Proofs (May 2012), http://afp.sf.net/entries/Separation_Algebra.shtml
Kolanski, R.: Verification of Programs in Virtual Memory Using Separation Logic. PhD thesis, School Comp. Sci. & Engin. (July 2011)
Tuch, H., Klein, G., Norrish, M.: Types, Bytes, and Separation Logic. In: Hofmann, M., Felleisen, M. (eds.) 34th POPL, Nice, France, pp. 97–108. ACM (January 2007)
Tuerk, T.: A Formalisation of Smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 469–484. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klein, G., Kolanski, R., Boyton, A. (2012). Mechanised Separation Algebra. In: Beringer, L., Felty, A. (eds) Interactive Theorem Proving. ITP 2012. Lecture Notes in Computer Science, vol 7406. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32347-8_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-32347-8_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32346-1
Online ISBN: 978-3-642-32347-8
eBook Packages: Computer ScienceComputer Science (R0)