Verifying concurrent graph algorithms

DOI10.1007/978-3-319-47958-3_17MaRDI QIDQ3179300zbMATH OpenOpenAlexFDO

Authors Azalea Raad, Aquinas Hobor, Jules Villard, Philippa Gardner

Publication date 21 December 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/10044/1/67346

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Graph theory (including graph drawing) in computer science (68R10) Parallel algorithms in computer science (68W10)

Recommendations

• ColoSL: concurrent local subjective logic
• Caper
• Automatically verifying concurrent queue algorithms
• Shape-Value Abstraction for Verifying Linearizability
• Inductive data flow graphs

Cites work

• ColoSL: concurrent local subjective logic
• Communicating state transition systems for fine-grained concurrent resources
• scientific article; zbMATH DE number 3541921 (Why is no real title available?)
• scientific article; zbMATH DE number 839542 (Why is no real title available?)
• Impredicative concurrent abstract predicates
• Local rely-guarantee reasoning
• The ramifications of sharing in data structures
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• Verifying concurrent graph algorithms
• Views, compositional reasoning for concurrent programs

Cited in

(9)

• Automated verification of the parallel Bellman-Ford algorithm
• ColoSL: concurrent local subjective logic
• Inductive data flow graphs
• Verifying concurrent graph algorithms
• Automated verification of parallel nested DFS
• Local reasoning for global graph properties
• scientific article; zbMATH DE number 7649962 (Why is no real title available?)
• Make flows small again: revisiting the flow framework
• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms

This page was built for publication: Verifying concurrent graph algorithms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3179300)