Verification of Certifying Computations through AutoCorres and Simpl
Certifying algorithms compute not only an output, but also a certificate that witnesses the correctness of the output for a particular input. A checker program uses this certificate to ascertain the correctness of the output. Recent work used the verification tools VCC and Isabelle to verify checker implementations and their mathematical background theory. The checkers verified stem from the widely-used algorithms library LEDA and are written in C. The drawback of this approach is the use of two tools. The advantage is that it could be carried out with reasonable effort in 2011.
In this article, we evaluate the feasibility of performing the entire verification within Isabelle. For this purpose, we consider checkers written in the imperative languages C and Simpl. We re-verify the checker for connectedness of graphs and present a verification of the LEDA checker for non-planarity of graphs. For the checkers written in C, we translate from C to Isabelle using the AutoCorres tool set and then argue in Isabelle, for the checkers written in Simpl, Isabelle is the only tool needed. We compare the new approach with the previous approach and discuss advantages and disadvantages.
An archive file with the sources of the verified checkers and their proofs is available here. They are intended to work with Isabelle 2012. They depend on AutoCorres 0.1, which in turn depends on the Simpl library from the AFP.