Sep 02, 2014: Jaco van de Pol: Mechanical Correctness Proof of Nested Depth First Search with Dafny

September 02, 2014Mechanical Correctness Proof of Nested Depth First Search with Dafny
Room: Carre 3HJaco van de Pol

The classical algorithm to detect accepting cycles in a directed graph is Nested Depth First Search (NDFS), solving the problem in linear time. NDFS is used to verify safety critical systems, so one might want a formal, machine checked correctness proof of this procedure. Dafny is an automated program verifier, that can prove the correctness of programs with respect to program annotations. The annotations are partly needed to specify the correctness criteria of the program, and partly to give hints to the automated prover.

In this interactive talk, the application of Dafny to prove the correctness of NDFS will be demonstrated. Starting point is a recursive formulation of the nested DFS procedure. Step by step, the complete correctness proof will be constructed. Along the way, several pros and cons of this and alternative approaches can be discussed.