A Simpl Shortest Path Checker Verification

ABSTRACT. Verifying the implementation of complex algorithms in reasonable time goes beyond the state of the art of current verification tools. Certifying algorithms compute in addition to each output a witness certifying that the output is correct. A checker for a certifying algorithm checks the witness for correctness and is usually much simpler than the algorithm. Verification of checkers is feasible with current tools and leads to computations that can be completely trusted.

Previous work verified several checkers from the algorithmic library LEDA using the interactive theorem prover Isabelle/HOL as a backend to the automatic code verifier VCC. Recent work shows that verification can be carried out completely within Isabelle/HOL and compares this with the previous approach concluding that this approach is more trustworthy with comparable efforts in the field of graph theory.

Here we use use the more recent framework and present a verification of a Simpl shortest path checker algorithm with nonnegative edge weights solely within Isabelle/HOL.