Reseña: “Certifying homological algorithms to study biomedical images”
Se ha presentado una Tesis doctoral de verificación formal con Coq/SSReflect titulada Certifying homological algorithms to study biomedical images.
Su autora es María Poza López de Echazarreta dirigida por César Domínguez y Julio Rubio (de la Universidad de la Rioja).
Su resumen es
In this memoir, we have reported on a research which provides a certified computation of homology groups associated with some digital images coming from a biomedical problem. The main contributions allowing us to reach this challenging goal have been the following ones.
- The implementation in Coq/SSReflect of the Romero-Sergeraert algorithm computing an admissible discrete vector field for a digital image.
- The complete formalization in Coq/SSReflect of the theorem known as Basic Perturbation Lemma (BPL).
- Two formalizations of the Vector-Field Reduction Theorem for matrices. One is proved using the BPL and the other one applying the Hexagonal Lemma.
- A discussion on different methods to overcome the efficiency problems appearing when executing programs inside proof assistants. In particular, the Haskell programming language has been used in two different ways: first, to model algorithms which are subsequently implemented in Coq and, second, as an oracle to produce results whose properties are verified in the proof assistant.
- A verified program to compute homology groups of a simplicial complex obtained from a digital image.
- As a by-product of all the other contributions, an application of Algebraic Topology to study biomedical images in a reliable manner. Our methodology ensures that the final homological calculations are correct.
By observing the memoir as a whole, it is clear that, even if our initial emphasis was in biomedical applications, much of the work has been devoted to the formalization of mathematics and program verification. The reason is that, even if we have built over very solid foundations (effective homology from the
algorithmic side and SSReflect as theorem proving basis), we needed to reproduce inside Coq/SSReflect a part of Computational Algebraic Topology. As a consequence, we focused on obtaining a complete verified path from biomedical digital images to homological computing, but without getting a good performance in the final implementation. Thus, our research should be considered as a proof of concept: homological image processing can be implemented in a verified manner by using interactive theorem provers. Our results are therefore rather a starting point, instead of a closed problem.
Un aspecto destacable es la metodología híbrida que se ha utilizado. Dicha metodología se explica en la página 24:
In our developments the formally certified implementation of the algorithms have followed the methodology presented in [Mörtberg 2010]. This methodology can be split into these three steps:
- Implement a version of our algorithms in Haskell, a lazy functional programming language.
- Test properties about the Haskell programs using QuickCheck. This tool allows one to test intensively properties about programs implemented in Haskell, in an automatic way.
- Verify the programs using Coq, an interactive proof assistant, and its SSReflect library.
Using QuickCheck can be considered as a good starting point towards the formal verification of our programs. This provides us two advantages:
- A specification of the properties which must be satisfied by our programs is given (a necessary step in the formalization process which will be reused
in Coq).- The testing process can be useful in order to detect bugs in a quick and easy way, before trying a formal verification of our programs (a quite difficult task).