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

    2 Citations (Scopus)


    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
    Number of pages16
    ISBN (Electronic)9783642393204
    ISBN (Print)9783642393198
    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

    Publication series

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


    ConferenceConferences on Intelligent Computer Mathematics: Calculemus 2013
    Abbreviated titleCICM 2013
    Country/TerritoryUnited Kingdom
    OtherHeld as Part of CICM 2013
    Internet address


    Dive into the research topics of 'Verifying a plaftorm for digital imaging: a multi-tool strategy'. Together they form a unique fingerprint.

    Cite this