Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras

DOI10.1007/978-3-030-43520-2_9OpenAlexW3013312844MaRDI QIDQ5098718

Walter Guttmann

Publication date: 30 August 2022

Published in: Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-43520-2_9

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• Unnamed Item
• Z
• Separation Logic
• Stone Algebras
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Towards pointer algebra
• Winskel is (almost) right: Towards a mechanized semantics textbook
• Reasoning algebraically about loops
• A completeness theorem for Kleene algebras and the algebra of regular events
• Parallel constructions of maximal path sets and applications to short superstrings
• Dijkstra, Floyd and Warshall meet Kleene
• Calculating with acyclic and cyclic lists
• Combining relational calculus and the Dijkstra-Gries method for deriving relational programs
• Verifying minimum spanning tree algorithms with Stone relation algebras
• Graphs, dioids and semirings. New models and algorithms.
• On Automated Program Construction and Verification
• Regular Algebra Applied to Path-finding Problems
• Reasoning about arrays
• Refinement Calculus
• Combinators for bi-directional tree transformations
• An improved equivalence algorithm
• An axiomatic basis for computer programming
• Relational and Kleene-Algebraic Methods in Computer Science
• On the calculus of relations

This page was built for publication: Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras