Local Reasoning for Global Graph Properties

DOI10.1007/978-3-030-44914-8_12OpenAlexW3023197541MaRDI QIDQ5041096

Siddharth Krishna, Thomas Wies, Alexander J. Summers

Publication date: 13 October 2022

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

Full work available at URL: https://arxiv.org/abs/1911.08632

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms

Uses Software

• Dafny
• VeriFast
• Toolchain
• Viper
• VACID-0
• GRASShopper
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Compositional entailment checking for a fragment of separation logic
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• CoLoSL: Concurrent Local Subjective Logic
• The ramifications of sharing in data structures
• Recursive proofs for inductive tree data-structures
• Verified Software Toolchain
• Dafny: An Automatic Program Verifier for Functional Correctness
• Verifying Concurrent Graph Algorithms
• Back to the future
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Bringing Order to the Separation Logic Jungle
• An Efficient Decision Procedure for Imperative Tree Data Structures
• Separation logic and abstraction
• Computer Science Logic
• Priority inheritance protocols: an approach to real-time synchronization
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science