On the Verification of the Correctness of a Subgraph Construction Algorithm

November 29, 2023 · The Ethereal · 🏛 International Conference on Verification, Model Checking and Abstract Interpretation

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Lucas Böltz, Viorica Sofronie-Stokkermans, Hannes Frey arXiv ID 2311.17860 Category cs.LO: Logic in CS Cross-listed cs.IT, cs.NI Citations 0 Venue International Conference on Verification, Model Checking and Abstract Interpretation Last Checked 5 months ago

Abstract

We automatically verify the crucial steps in the original proof of correctness of an algorithm which, given a geometric graph satisfying certain additional properties removes edges in a systematic way for producing a connected graph in which edges do not (geometrically) intersect. The challenge in this case is representing and reasoning about geometric properties of graphs in the Euclidean plane, about their vertices and edges, and about connectivity. For modelling the geometric aspects, we use an axiomatization of plane geometry; for representing the graph structure we use additional predicates; for representing certain classes of paths in geometric graphs we use linked lists.