How to Trust the Output of Your Program

Spotlight: Released Monday, 6 May 2013

Adrian Neumann, Jens Schmidt and Christine Rizkallah

Transferring an algorithm (i.e. a solution procedure, which is usually given as a natural language description) to computer code is difficult and error prone. Even moderately difficult algorithms need programs with thousands of lines of code. For that reason, the code may contain many mistakes, and subtle errors can be very hard to find. For example, the planarity test in LEDA contained an error that was only discovered after years of intensive use.

The field of Software Engineering has developed many tools to improve the quality of code. A standard practice, for example, is extensive testing. This requires a diverse set of inputs with known solutions. Often this is hard to come by, as, intuitively, the program wouldn't be needed if finding the correct answers for example inputs were easy. Certifying algorithms approach the problem from a different angle. Instead of trying to improve the quality of implementations, certifying algorithms improve the methods to solve the problem such that the implementation is easier to check for correctness. This is achieved by enhancing the algorithms in order to provide a certificate that proves that their answer is correct; i.e., the algorithm does not provide only a bare yes-or-no answer to the question (e.g. "yes, this graph is planar" or "no, this graph is not planar"), but also gives a reason for this answer. The certificate is structured such that a much simpler program, the checker, can verify its correctness. Only the checker needs to be carefully examined for correctness. An important goal of certifying algorithms is to find certificates that are so simple that the checker can be formally verified, that is, one can give a mathematical proof that the code (not just its description) is correct. Formal verification, unlike mere testing, guarantees the absence of errors, but is impractical for most real-world programs. Through certifying algorithms we can use this powerful technique to prove that our algorithm's answers are always correct if the checker agrees with them. Developing certifying algorithms is a major goal for problems where the fastest solutions known are complicated, as correct implementations of these solutions are hard to write. Having a certifying algorithm for such a problem allows verifying the output of every particular instance, regardless of how complicated the computation of this output is. For this reason, certifying algorithms are now used in software libraries like LEDA for reliability purposes. Current Research Problems Prominent examples of problems whose fastest known solutions are complicated include testing a graph for 3-connectivity and for 3-edge-connectivity. These problems are important for various applications in the areas of graph drawing and graph embeddings and for validating 3D-polytopes. Although sophisticated linear-time solutions for these problems have been known for decades, none of them describe an easy-to-verify certificate. A natural certificate to prove 3-connectivity is a so-called construction sequence. For a 3-connected graph G, a construction sequence is a sequence of certain operations that constructs G, when applied to K4. The currently fastest algorithms that certify 3-connectivity need O(|V|2) time and use construction sequences as certificates.