A Simpl Shortest Path Checker Verification

Abstract. Verification of complex algorithms with current verification tools in reasonable time is challenging. Certifying algorithms compute not only an output but also a witness certifying that the output is correct. A checker for a certify-ing algorithm is a simple program that decides whether the witness is correct for a particular input and output. Verification of checkers is feasible and leads to trustworthy computations. In previous work, we verified checkers from the al-gorithmic library LEDA using the interactive theorem prover Isabelle/HOL as a backend to the automatic code verifier VCC. More recently, we showed that ver-ification can be carried out completely within Isabelle/HOL and compared this to the previous approach. We concluded that the more recent approach is more trustworthy with comparable efforts. Here we implement a shortest path checker algorithm for graphs with nonnegative edge weights in the imperative pseudo-code language Simpl. Moreover, we use the more recent framework and formally verify the checker using Isabelle/HOL.