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
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.
Conference Manager (V2.56.8 - Rev. 399)