Trustworthy Graph Algorithms
This addresses the need for trustworthy algorithms in computer science, but it is incremental as it builds on existing verification methods.
The LEDA project aimed to create a reliable library of graph and geometric algorithms, and this work applied formal program verification to enhance trustworthiness, specifically verifying the blossom-shrinking algorithm for maximum cardinality matching.
The goal of the LEDA project was to build an easy-to-use and extendable library of correct and efficient data structures, graph algorithms and geometric algorithms. We report on the use of formal program verification to achieve an even higher level of trustworthiness. Specifically, we report on an ongoing and largely finished verification of the blossom-shrinking algorithm for maximum cardinality matching.