Abstract Interpretation of Graphs.

Path problems in graphs can be solved by abstraction of a fixpoint definition of all paths in a finite graph. Applied to the Roy-Floyd-Warshall shortest path algorithm this yields a naïve $$n^4$$ algorithm where n is the number of graph vertices. By over-approximating the elementary paths and cycles and generalizing the classical exact fixpoint abstraction, we constructively derive the classical $$n^3$$ Roy-Floyd-Warshall algorithm.