Reseña: Refinement based verification of imperative data structures

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Refinement based verification of imperative data structures

Su autor es Peter Lammich (de la Chair for Logic and Verification en la Univ. técnica de Munich).

Su resumen es

In this paper we present a stepwise refinement based top-down approach to verified imperative data structures. Our approach is modular in the sense that already verified data structures can be used for construction of more complex data structures. Moreover, our data structures can be used as building blocks for the verification of algorithms. Our tool chain supports refinement down to executable code in various programming languages, and is fully implemented in Isabelle/HOL, such that its trusted code base is only the inference kernel and the code generator of Isabelle/HOL.

As a case study, we verify an indexed heap data structure, and use it to generate an efficient verified implementation of Dijkstra’s algorithm.

El trabajo se ha presentado en el CPP 2016 (The 5th ACM SIGPLAN Conference on Certified Programs and Proofs).

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.