Aarhus University Seal / Aarhus Universitets segl

Design patterns in separation logic

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Neelakantan R. Krishnaswami, Carnegie Mellon University, Unknown
  • Jonathan Aldrich, Carnegie Mellon University, Unknown
  • Lars Birkedal
  • Kasper Svendsen, IT University of Copenhagen, Denmark
  • Alexandre Buisse, IT University of Copenhagen, Unknown

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.

Original languageEnglish
Title of host publicationProceedings of the 2009 ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI'09
EditorsAndrew Kennedy, Amal Ahmed
Number of pages11
PublisherAssociation for Computing Machinery
Publication year14 Jul 2009
Pages105-115
ISBN (print)9781605584201
DOIs
Publication statusPublished - 14 Jul 2009
Externally publishedYes

    Research areas

  • Design Patterns, Formal Verification, Separation Logic

See relations at Aarhus University Citationformats

ID: 81389331