Design and formal proof of a new optimal image segmentation program with hypermaps |
| |
| Authors: | Jean-François Dufourd [Author Vitae] |
| |
| Affiliation: | Université Louis-Pasteur de Strasbourg UFR de Mathématique et d’Informatique, Laboratoire des Sciences de l’Image, de l’Informatique et de la Télédétection (LSIIT, UMR CNRS-ULP 7005), Pôle API, Boulevard Sébastien Brant, 67400 Illkirch, France |
| |
| Abstract: | This article presents the design of a new functional 2D image segmentation algorithm by cell merging in a subdivision, its proof of total correctness, and the derivation of an optimal imperative program. The planar subdivisions are modeled by hypermaps. The formal specifications of hypermaps and segmentation are developed in the Calculus of Inductive Constructions. The proofs are assisted by the Coq system. The final program is written in C. |
| |
| Keywords: | Image segmentation Hypermaps Formal specification Coq system Computer-aided correctness proof |
| 本文献已被 ScienceDirect 等数据库收录！ |
