Design Patterns in Separation Logic

Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kaspar Svendsen and Alexandre Buisse

The ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2009)
Savannah, Georgia, USA, Saturday, 24 January, 2009

---

Abstract

Object-oriented programs are notable for making use of both higher-order abstractions and mutable, aliased state. Either feature alone is challenging for formal verification, and the combination yields very flexible program designs and correspondingly difficult verification problems. In this paper, we show how to formally specify and verify programs that use several common design patterns in concert.

---

START Conference Manager (V2.56.8 - Rev. 399)