Verifying a plaftorm for digital imaging: A multi-tool strategy

  1. Heras, J. 2
  2. Mata, G. 1
  3. Romero, A. 1
  4. Rubio, J. 1
  5. Sáenz, R. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

  2. 2 University of Dundee
    info

    University of Dundee

    Dundee, Reino Unido

    ROR https://ror.org/03h2bxq36

Revista:
Lecture Notes in Computer Science

ISSN: 0302-9743

Año de publicación: 2013

Volumen: 7961 LNAI

Páginas: 66-81

Tipo: Artículo

DOI: 10.1007/978-3-642-39320-4_5 SCOPUS: 2-s2.0-84880748074 arXiv: 1303.1420v2 GOOGLE SCHOLAR lock_openAcceso abierto editor

Otras publicaciones en: Lecture Notes in Computer Science

Proyectos relacionados

Gestión Mecanizada del Conocimiento Matemático. Aplicaciones en Topología Algebraica y en Lógica.

2009/00207/001

Resumen

Fiji is a Java platform widely used by biologists and other experimental scientists to process digital images. In our research, made together with a biologists team, we use Fiji in some pre-processing steps before undertaking a homological digital processing of images. In a previous work, we have formalised the correctness of the programs which use homological techniques to analyse digital images. However, the verification of Fiji's pre-processing step was missed. In this paper, we present a multi-tool approach (based on the combination of Why/Krakatoa, Coq and ACL2) filling this gap. © 2013 Springer-Verlag Berlin Heidelberg.