Mapped Separation Logic

Rafal Kolanski and Gerwin Klein

Abstract

We present Mapped Separation Logic, an instance of Separation Logic for reasoning about virtual memory. Our logic is formalised in the Isabelle/HOL theorem prover and it allows reasoning on properties about page tables, direct physical memory access, virtual memory access, and shared memory. Mapped Separation Logic fully supports all rules of abstract Separation Logic, including the frame rule.

Online Copy

Available as [PDF]

Bibtex entry

	@InProceedings{Kolanski_Klein_08,
	  author =    {Rafal Kolanski and Gerwin Klein},
	  title =     {Mapped Separation Logic},
	  booktitle = {Second IFIP Working Conference on
	  Verified Software: Theories, Tools, and Experiments (VSTTE 2008)},
	  editor =    {Jim Woodcock and Natarajan Shankar},
	  series =    {LNCS},
	  publisher =  {Springer},
	  volume =    5295,
	  pages =	 {15--29},
	  year =      {2008},
	  isbn =	 {978-3-540-87872-8},
	  address =   {Toronto, Canada},
	  month =     Oct,
	}
Gerwin Klein
2008-12-22