A certifying algorithm provides in addition to its output y for an input x also a witness w proving that y is the correct output for x. A sample certifying algorithm is a graph planarity tester that not only outputs whether the input graph is correct but also an embedding or a Kuratowski sub-graph, depending on the input being planar or not. Another example is a linear programming solver that yields an optimal solution plus a solution to the dual problem. Certifying algorithms originate from the development of the LEDA library. For an algorithm to be certifying, a (typically simple) checker is employed to check that w proves that y is the correct output of x. Various algorithms have certifying variants that often have the same run-time as the original algorithm. Rather than verifying the code of an algorithm—a hard and challenging task in program verification—the correctness of certifying algorithms can be obtained by formally verifying the checker. This more manageable verification task has been successfully applied to various certifying algorithms by combining code verification and theorem proving using theorem provers such as Isabelle or Coq.

This dissertation project focuses on certifying randomised algorithms. This topic has several aspects. Whereas a few certifying randomised algorithms do exist, the formal verification of checkers for certifying randomised algorithms is an open problem and has not been addressed. In addition, certifying variants of prominent efficient randomised algorithms such as Karger’s min-cut algorithm are so far unknown. This in particular applies to randomised algorithms that provide outputs with a certain (small) probability. The central idea is to allow for randomised certification and to exploit for certifying randomised algorithms with positive error probability (Monte Carlo). This can be done either using checkers that are fully correct, or by exploiting checkers that make errors with a small probability, guaranteeing the correctness of a certain output with a high probability. In both settings, the correctness of the checker is to be formally verified. Possible promising techniques for this are probabilistic program verification and theorem proving equipped for randomisation. Within this dissertation project, a formal framework for the verification of certifying randomised algorithms is to be developed, so far uncertified randomised algorithms are to be certified, and new efficient randomised algorithms amenable to certification need to be designed.