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

Aldizkaria:
Lecture Notes in Computer Science

ISSN: 0302-9743

Argitalpen urtea: 2013

Alea: 7961 LNAI

Orrialdeak: 66-81

Mota: Artikulua

beta Ver similares en nube de resultados
DOI: 10.1007/978-3-642-39320-4_5 SCOPUS: 2-s2.0-84880748074 arXiv: 1303.1420v2 GOOGLE SCHOLAR lock_openSarbide irekia editor

Beste argitalpen batzuk: Lecture Notes in Computer Science

Lotura duten proiektuak

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

2009/00207/001

Laburpena

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.