Reseña: A framework for verifying depth-first search algorithms in Isabelle/HOL
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado A framework for verifying depth-first search algorithms in Isabelle/HOL.
Sus autores son Peter Lammich y René Neumann (de la Technische Universität München)
Su resumen es
Many graph algorithms are based on depth-first search (DFS).The formalizations of such algorithms typically share many common ideas. In this paper, we summarize these ideas into a framework in Isabelle/HOL.
Building on the Isabelle Refinement Framework, we provide support for a refinement based development of DFS based algorithms, from phrasing and proving correct the abstract algorithm, over choosing an adequate implementation style (e. g., recursive, tail-recursive), to creating an executable algorithm that uses efficient data structures.
As a case study, we verify DFS based algorithms of different complexity, from a simple cyclicity checker, over a safety property model checker, to complex algorithms like nested DFS and Tarjan’s SCC algorithm.
El trabajo se ha presentado en The 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015)
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.