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. © 2012 Springer-Verlag.
Author supplied keywords
Cite
CITATION STYLE
Klein, G., Kolanski, R., & Boyton, A. (2012). Mechanised separation algebra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7406 LNCS, pp. 332–337). https://doi.org/10.1007/978-3-642-32347-8_22
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
