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 proceedingConference contribution

    1 Citation (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 languageEnglish
    Title of host publicationIntelligent Computer Mathematics
    Subtitle of host publicationMKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings
    EditorsJacques Carette, David Aspinall, Christoph Lange, Petr Sojka, Wolfgang Windsteiger
    Place of PublicationBerlin
    PublisherSpringer
    Pages66-81
    Number of pages16
    ISBN (Electronic)9783642393204
    ISBN (Print)9783642393198
    DOIs
    Publication statusPublished - 2013
    EventConferences on Intelligent Computer Mathematics: Calculemus 2013 - University of Bath in Building 8W, Bath, United Kingdom
    Duration: 8 Jul 201312 Jul 2013
    http://www.cicm-conference.org/2013/cicm.php

    Publication series

    NameLecture notes in computer science
    PublisherSpringer
    Volume7961
    ISSN (Print)0302-9743

    Conference

    ConferenceConferences on Intelligent Computer Mathematics: Calculemus 2013
    Abbreviated titleCICM 2013
    CountryUnited Kingdom
    CityBath
    Period8/07/1312/07/13
    OtherHeld as Part of CICM 2013
    Internet address

    Fingerprint

    Imaging techniques
    Processing
    Digital signal processing

    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). Berlin: Springer . https://doi.org/10.1007/978-3-642-39320-4_5
    Heras, Jonathan ; Mata, Gadea ; Romero, Ana ; Rubio, Julio ; Sáenz, Rubén . / 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",

    }

    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; Rubio, Julio; Sáenz, Rubén .

    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 proceedingConference contribution

    TY - GEN

    T1 - Verifying a plaftorm for digital imaging

    T2 - a multi-tool strategy

    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

    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

    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). https://doi.org/10.1007/978-3-642-39320-4_5