Design patterns in separation logic

Object-oriented programs are notable for making use of both rder 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. Categories and Subject Descriptors F.3 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; D.2.8 [Software Engineering]: Metrics—complexity measures, performance measures General Terms Languages, Verification Keywords Separation Logic, Design Patterns, Formal Verification

• Type: Conference
• Year: 2009
• Where: TLDI
• Authors: Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, Alexandre Buisse
• Keywords: Common Design Patterns, Formal Methods, Keywords Separation Logic, Measures General Terms, TLDI 2009