Aarhus University Seal / Aarhus Universitets segl

Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency

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

  • Aaron Turon, MPI-SWS, Saarbruecken, Germany
  • Derek Dreyer , MPI-SWS, Saarbruecken, Germany
  • Lars Birkedal
Modular programming and modular verification go hand in hand, but most existing logics for concurrency ignore two crucial forms of modularity: *higher-order functions*, which are essential for building reusable components, and *granularity abstraction*, a key technique for hiding the intricacies of fine-grained concurrent data structures from the clients of those data structures. In this paper, we present CaReSL, the first logic to support the use of granularity abstraction for modular verification of higher-order concurrent programs. After motivating the features of CaReSL through a variety of illustrative examples, we demonstrate its effectiveness by using it to tackle a significant case study: the first formal proof of (partial) correctness for Hendler et al.'s "flat combining" algorithm.
Original languageEnglish
Title of host publicationProceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13
EditorsGreg Morrisett, Tarmo Uustalu
Number of pages14
PublisherAssociation for Computing Machinery
Publication year2013
ISBN (print)978-1-4503-2326-0
Publication statusPublished - 2013
Event ACM SIGPLAN International Conference on FunctionalPprogramming - Boston, Massachusetts, United States
Duration: 25 Sep 201327 Sep 2013
Conference number: 18


Conference ACM SIGPLAN International Conference on FunctionalPprogramming
LandUnited States
ByBoston, Massachusetts

See relations at Aarhus University Citationformats

ID: 68506195