Reseña: A framework for verified depth-first algorithms
En el CPP 2015 Peter Lammich y René Neumann presentarán el trabajo A framework for verifying depth-first search algorithms que está basado en el de René Neumann titulado A framework for verified depth-first algorithms.
El resumen de este último es
We present a framework in Isabelle/HOL for formalizing variants of depth-first search. This framework allows to easily prove non-trivial properties of these variants. Moreover, verified code in several programming languages including Haskell, Scala and Standard ML can be generated. In this paper, we present an abstract formalization of depth-first search and demonstrate how it is refined to an efficiently executable version. Further we use the emptiness-problem of Büchi-automata known from model checking as the motivation to present three Nested DFS algorithms. They are formalized, verified and transformed into executable code using our framework.
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.