Caper: Automatic Verification for Fine-Grained Concurrency

Publication: Research - peer-reviewArticle in proceedings

Recent program logics based on separation logic emphasise a modular approach to proving functional correctness for fine-grained concurrent programs. However, these logics have no automation support. In this paper, we present Caper, a prototype tool for automated reason- ing in such a logic. Caper is based on symbolic execution, integrating reasoning about interference on shared data and about ghost resources that are used to mediate this interference. This enables Caper to verify the functional correctness of fine-grained concurrent algorithms.
Original languageEnglish
Title of host publicationProceedings of the 26th European Symposium on Programming
Number of pages27
Publication year22 Apr 2017
StatePublished - 22 Apr 2017
EventEuropean Symposium on Programming - Uppsala, Sweden

Conference

ConferenceEuropean Symposium on Programming
Nummer26
Locationhttp://www.etaps.org/index.php/2017/esop
LandSweden
ByUppsala
Periode22/04/201729/04/2017

See relations at Aarhus University Citationformats

ID: 107771883