Reseña: Correctness of pointer manipulating algorithms illustrated by a verified BDD construction
Se ha publicado un nuevo trabajo de verificación formal en Isabelle/HOL titulado Correctness of pointer manipulating algorithms illustrated by a verified BDD construction.
Los autores del trabajo son Mathieu Giorgino y Martin Strecker (de la Univ. de Toulouse).
El trabajo se presentará el 29 de agosto en el FM 2012 (18th International Symposium on Formal Methods).
En el trabajo se presenta una metodología para la verificación de programas imperativos usando el asistente de prueba Isabelle/HOL y su extensión Imperative_HOL, junto con el generador de código Scala de Isabelle. Como aplicación de la metodología se verifica los diagramas de decisión binarios (BDD).
Su resumen es
This paper is an extended case study using a high-level approach to the verification of graph transformation algorithms: To represent sharing, graphs are considered as trees with additional pointers, and algorithms manipulating them are essentially primitive recursive traversals written in a monadic style. With this, we achieve almost trivial termination arguments and can use inductive reasoning principles for showing the correctness of the algorithms. We illustrate the approach with the verification of a BDD package which is modular in that it can be instantiated with different implementations of association tables for node lookup. We have also implemented a garbage collector for freeing association tables from unused entries. Even without low-level optimizations, the resulting implementation is reasonably efficient.
El código de la formalización se encuentra en aquí
El trabajo es parte del proyecto CLIMT (Categorical and Logical Methods in Model Transformation).