IRUS Total

Verifying concurrent graph algorithms

File Description SizeFormat 
main.pdfPublished version566.13 kBAdobe PDFView/Open
Raad2016Verifying.pdfSubmitted version566.13 kBAdobe PDFView/Open
Title: Verifying concurrent graph algorithms
Authors: Raad, A
Hobor, A
Villard, J
Gardner, P
Item Type: Conference Paper
Abstract: 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.
Issue Date: 9-Oct-2016
Date of Acceptance: 16-Aug-2016
URI: http://hdl.handle.net/10044/1/67346
DOI: https://dx.doi.org/10.1007/978-3-319-47958-3_17
ISSN: 0302-9743
Publisher: Springer Verlag
Start Page: 314
End Page: 334
Journal / Book Title: Lecture Notes in Computer Science
Volume: 10017
Copyright Statement: © Springer International Publishing AG 2016. The final publication is available at Springer via https://link.springer.com/chapter/10.1007%2F978-3-319-47958-3_17
Sponsor/Funder: Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Funder's Grant Number: EP/K008528/1 - RG65358
Conference Name: Asian Symposium on Programming Languages and Systems
Keywords: 08 Information And Computing Sciences
Artificial Intelligence & Image Processing
Publication Status: Published
Start Date: 2016-11-21
Finish Date: 2016-11-23
Conference Place: Hanoi, Vietnam
Appears in Collections:Computing
Faculty of Engineering