Caper: automatic verification for fine-grained concurrency
File(s)caper.pdf (458.36 KB)
Accepted version
Author(s)
Dinsdale-Young, T
da Rocha Pinto, P
Just Andersen, K
Birkedal, L
Type
Conference Paper
Abstract
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 reasoning 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.
Date Issued
2017-03-19
Date Acceptance
2016-12-17
Citation
Lecture Notes in Computer Science, 2017, pp.420-447
ISBN
9783662544341
ISSN
0302-9743
Publisher
Springer Verlag
Start Page
420
End Page
447
Journal / Book Title
Lecture Notes in Computer Science
Copyright Statement
© Springer-Verlag GmbH Germany 2017. he final publication is available at Springer via https://link.springer.com/chapter/10.1007%2F978-3-662-54434-1_16
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Grant Number
EP/H008373/1
EP/H008373/1
EP/K008528/1 - RG65358
EP/K008528/1
Source
26th European Symposium on Programming, ESOP 2017
Subjects
Artificial Intelligence & Image Processing
Publication Status
Published
Start Date
2017-04-22
Finish Date
2017-04-29
Coverage Spatial
Uppsala, Sweden
Date Publish Online
2017-03-19