Aarhus University Seal / Aarhus Universitets segl

Joins: A case study in modular specification of a concurrent reentrant higher-order library

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

  • Kasper Svendsen, IT University of Copenhagen, Denmark
  • Lars Birkedal
  • Matthew Parkinson, Microsoft Research, Cambridge, Unknown
We present a case study of formal specification for the C joins library, an advanced concurrent library implemented using both shared mutable state and higher-order methods. The library is specified and verified in HOCAP, a higher-order separation logic extended with a higher-order variant of concurrent abstract predicates.
Original languageEnglish
Title of host publication27th European Conference on Object-Oriented Programming, ECOOP 2013; Montpellier; France
EditorsGiuseppe Castagna
Number of pages25
PublisherSpringer
Publication year16 Jul 2013
Pages327-351
ISBN (print)9783642390371
ISBN (Electronic)978-3-642-39038-8
DOIs
Publication statusPublished - 16 Jul 2013
Externally publishedYes
EventEuropean Conference on Object-Oriented Programming - Montpellier, France
Duration: 1 Jul 20135 Jul 2013
Conference number: 27

Conference

ConferenceEuropean Conference on Object-Oriented Programming
Nummer27
LandFrance
ByMontpellier
Periode01/07/201305/07/2013
SeriesLecture Notes in Engineering and Computer Science
Volume7920
ISSN2078-0958

See relations at Aarhus University Citationformats

ID: 81354150