Aarhus University Seal / Aarhus Universitets segl

Verifying generics and delegates

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

  • Kasper Svendsen, IT University of Copenhagen, Denmark
  • Lars Birkedal
  • Matthew Parkinson, University of Cambridge, United Kingdom

Recently, object-oriented languages, such as C , have been extended with language features prevalent in most functional languages: parametric polymorphism and higher-order functions. In the OO world these are called generics and delegates, respectively. These features allow for greater code reuse and reduce the possibilities for runtime errors. However, the combination of these features pushes the language beyond current object-oriented verification techniques. In this paper, we address this by extending a higher-order separation logic with new assertions for reasoning about delegates and variables. We faithfully capture the semantics of C delegates including their capture of the l-value of a variable, and that "stack" variables can live beyond their "scope". We demonstrate that our logic is sound and illustrate its use by specifying and verifying a series of interesting and challenging examples.

Original languageEnglish
Title of host publicationECOOP 2010 – Object-Oriented Programming : 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings
Number of pages25
Publication year3 Aug 2010
ISBN (print)9783642141065
ISBN (Electronic)978-3-642-14107-2
Publication statusPublished - 3 Aug 2010
Externally publishedYes
EventEuropean Conference on Object-Oriented Programming. ECOOP 2010 - Maribor, Slovenia
Duration: 21 Jun 201025 Jun 2010
Conference number: 24


ConferenceEuropean Conference on Object-Oriented Programming. ECOOP 2010
SeriesLecture Notes in Computer Science

See relations at Aarhus University Citationformats

ID: 81388780