Verification of a Subgraph Construction Algorithm for Geometric Graphs - VMCAI 2024

Explore an 18-minute conference talk from ACM SIGPLAN's VMCAI'24 that delves into the automatic verification of a subgraph construction algorithm. Learn how researchers Lucas Böltz, Viorica Sofronie-Stokkermans, and Hannes Frey tackle the challenge of verifying crucial steps in the original proof of correctness for an algorithm that systematically removes edges from geometric graphs to produce connected, non-intersecting graphs. Discover the innovative approaches used to model and reason about both geometric properties of graphs in the Euclidean plane and graph connectivity. Gain insights into the use of plane geometry axiomatization, additional predicates for graph structure representation, and linked lists for modeling specific path classes in geometric graphs.