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{Raad:2016:10.1007/978-3-319-47958-3_17,
author = {Raad, A and Hobor, A and Villard, J and Gardner, P},
doi = {10.1007/978-3-319-47958-3_17},
pages = {314--334},
publisher = {Springer Verlag},
title = {Verifying concurrent graph algorithms},
url = {http://dx.doi.org/10.1007/978-3-319-47958-3_17},
year = {2016}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - We show how to verify four challenging concurrent fine-grained graph-manipulating algorithms, including graph copy, a speculatively parallel Dijkstra, graph marking and spanning tree. We develop a reasoning method for such algorithms that dynamically tracks the contributions and responsibilities of each thread operating on a graph, even in cases of arbitrary recursive thread creation. We demonstrate how to use a logic without abstraction ( Open image in new window ) to carry out abstract reasoning in the style of iCAP, by building the abstraction into the proof structure rather than incorporating it into the semantic model of the logic.
AU  - Raad,A
AU  - Hobor,A
AU  - Villard,J
AU  - Gardner,P
DO  - 10.1007/978-3-319-47958-3_17
EP  - 334
PB  - Springer Verlag
PY  - 2016///
SN  - 0302-9743
SP  - 314
TI  - Verifying concurrent graph algorithms
UR  - http://dx.doi.org/10.1007/978-3-319-47958-3_17
UR  - http://hdl.handle.net/10044/1/67346
ER  -
Download