Imperial College London
Alternate

ProfessorPhilippaGardner

Faculty of Engineering, Department of Computing

Professor of Theoretical Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8292p.gardner Website

 
 
//

Location

 

453Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Dinsdale-Young:2017:10.1007/978-3-662-54434-1_16,
author = {Dinsdale-Young, T and da, Rocha Pinto P and Just, Andersen K and Birkedal, L},
doi = {10.1007/978-3-662-54434-1_16},
pages = {420--447},
publisher = {Springer Verlag},
title = {Caper: automatic verification for fine-grained concurrency},
url = {http://dx.doi.org/10.1007/978-3-662-54434-1_16},
year = {2017}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - Dinsdale-Young,T
AU  - da,Rocha Pinto P
AU  - Just,Andersen K
AU  - Birkedal,L
DO  - 10.1007/978-3-662-54434-1_16
EP  - 447
PB  - Springer Verlag
PY  - 2017///
SN  - 0302-9743
SP  - 420
TI  - Caper: automatic verification for fine-grained concurrency
UR  - http://dx.doi.org/10.1007/978-3-662-54434-1_16
UR  - http://hdl.handle.net/10044/1/43741
ER  -
Download