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

Jonathan Heras; Gadea Mata; Ana Romero; Julio Rubio; Rubén  Sáenz

doi:10.1007/978-3-642-39320-4_5

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

Jonathan Heras, Gadea Mata, Ana Romero, Julio Rubio, Rubén Sáenz

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	Intelligent Computer Mathematics
Subtitle of host publication	MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings
Editors	Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, Wolfgang Windsteiger
Place of Publication	Berlin
Publisher	Springer
Pages	66-81
Number of pages	16
ISBN (Electronic)	9783642393204
ISBN (Print)	9783642393198
DOIs	https://doi.org/10.1007/978-3-642-39320-4_5
Publication status	Published - 2013
Event	Conferences on Intelligent Computer Mathematics: Calculemus 2013 - University of Bath in Building 8W, Bath, United Kingdom Duration: 8 Jul 2013 → 12 Jul 2013 http://www.cicm-conference.org/2013/cicm.php

Publication series

Name	Lecture notes in computer science
Publisher	Springer
Volume	7961
ISSN (Print)	0302-9743

Conference

Conference	Conferences on Intelligent Computer Mathematics: Calculemus 2013
Abbreviated title	CICM 2013
Country/Territory	United Kingdom
City	Bath
Period	8/07/13 → 12/07/13
Other	Held as Part of CICM 2013
Internet address	http://www.cicm-conference.org/2013/cicm.php

Access to Document

10.1007/978-3-642-39320-4_5

Cite this

Heras, J., Mata, G., Romero, A., Rubio, J., & Sáenz, R. (2013). Verifying a plaftorm for digital imaging: a multi-tool strategy. In J. Carette, D. Aspinall, C. Lange, P. Sojka, & W. Windsteiger (Eds.), Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings (pp. 66-81). (Lecture notes in computer science; Vol. 7961). Springer . https://doi.org/10.1007/978-3-642-39320-4_5

Heras, Jonathan ; Mata, Gadea ; Romero, Ana et al. / Verifying a plaftorm for digital imaging : a multi-tool strategy. Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. editor / Jacques Carette ; David Aspinall ; Christoph Lange ; Petr Sojka ; Wolfgang Windsteiger. Berlin : Springer , 2013. pp. 66-81 (Lecture notes in computer science).

@inproceedings{2ada05fb6ca447a6be60da87f275946d,

title = "Verifying a plaftorm for digital imaging: a multi-tool strategy",

abstract = "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.",

author = "Jonathan Heras and Gadea Mata and Ana Romero and Julio Rubio and Rub{\'e}n S{\'a}enz",

year = "2013",

doi = "10.1007/978-3-642-39320-4_5",

language = "English",

isbn = "9783642393198",

series = "Lecture notes in computer science",

publisher = "Springer ",

pages = "66--81",

editor = "Carette, {Jacques } and Aspinall, {David } and Lange, {Christoph } and Sojka, {Petr } and Windsteiger, {Wolfgang }",

booktitle = "Intelligent Computer Mathematics",

note = "Conferences on Intelligent Computer Mathematics: Calculemus 2013, CICM 2013 ; Conference date: 08-07-2013 Through 12-07-2013",

url = "http://www.cicm-conference.org/2013/cicm.php",

}

Heras, J, Mata, G, Romero, A, Rubio, J & Sáenz, R 2013, Verifying a plaftorm for digital imaging: a multi-tool strategy. in J Carette, D Aspinall, C Lange, P Sojka & W Windsteiger (eds), Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. Lecture notes in computer science, vol. 7961, Springer , Berlin, pp. 66-81, Conferences on Intelligent Computer Mathematics: Calculemus 2013, Bath, United Kingdom, 8/07/13. https://doi.org/10.1007/978-3-642-39320-4_5

Verifying a plaftorm for digital imaging: a multi-tool strategy. / Heras, Jonathan; Mata, Gadea; Romero, Ana et al.
Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. ed. / Jacques Carette; David Aspinall; Christoph Lange; Petr Sojka; Wolfgang Windsteiger. Berlin: Springer , 2013. p. 66-81 (Lecture notes in computer science; Vol. 7961).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Verifying a plaftorm for digital imaging

T2 - Conferences on Intelligent Computer Mathematics: Calculemus 2013

AU - Heras, Jonathan

AU - Mata, Gadea

AU - Romero, Ana

AU - Rubio, Julio

AU - Sáenz, Rubén

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84880748074&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-39320-4_5

DO - 10.1007/978-3-642-39320-4_5

M3 - Conference contribution

AN - SCOPUS:84880748074

SN - 9783642393198

T3 - Lecture notes in computer science

SP - 66

EP - 81

BT - Intelligent Computer Mathematics

A2 - Carette, Jacques

A2 - Aspinall, David

A2 - Lange, Christoph

A2 - Sojka, Petr

A2 - Windsteiger, Wolfgang

PB - Springer

CY - Berlin

Y2 - 8 July 2013 through 12 July 2013

ER -

Heras J, Mata G, Romero A, Rubio J, Sáenz R. Verifying a plaftorm for digital imaging: a multi-tool strategy. In Carette J, Aspinall D, Lange C, Sojka P, Windsteiger W, editors, Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings. Berlin: Springer . 2013. p. 66-81. (Lecture notes in computer science). doi: 10.1007/978-3-642-39320-4_5

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)