How to Trust the Output of Your Program

Adrian Neumann & Christine Rizkallah & Jens M. Schmidt

How to Trust the Output of Your Program

A construction sequence of a 3-connected graph G

Transferring an algorithm (i.e. a solution procedure to computer code is difficult and error prone. 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 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 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, 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 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. Having a certifying algorithm for such a problem allows verifying the output of every 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. Although 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 operations that constructs G, when applied to K4.

We proposed the first linear-time certifying algorithm for testing a graph for 3-connectivity. The algorithm has been implemented and made publicly available. By using a well-known reduction from edge-connectivity to vertexconnectivity, we can obtain a linear-time certifying algorithm for 3-edge-connectivity.

A current research problem is to find a direct certificate for 3-edge-connectivity. Future open questions include finding certificates for k-connectivity or k-edge-connectivity for k 4.

Verification of Checkers

We developed a framework for verifying checkers. This guarantees instance correctness of all certifying algorithms whose certificates can be checked by this framework. We applied the framework to several examples from the LEDA library in the field of graph theory. Currently, we are evaluating alternative tools for the verification framework and comparing the results in terms of trust and effort needed.