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

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

Recommendations

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

Cites work

• scientific article; zbMATH DE number 3541921 (Why is no real title available?)
• scientific article; zbMATH DE number 839542 (Why is no real title available?)
• ColoSL: concurrent local subjective logic
• Communicating state transition systems for fine-grained concurrent resources
• 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)

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

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)