Verifying a platform for digital imaging: a multi-tool strategy
This work addresses verification gaps for biologists and experimental scientists using Fiji, but it is incremental as it builds on prior formalization efforts.
The authors tackled the problem of verifying Fiji's pre-processing steps for digital image analysis, which was previously unverified, by developing a multi-tool approach using Why/Krakatoa, Coq, and ACL2 to ensure correctness.
Fiji is a Java platform widely used by biologists and other experimental scientists to process digital images. In particular, 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 filling this gap, based on the combination of Why/Krakatoa, Coq and ACL2.