Formal verification of bioinformatics software using model checking and theorem proving.

Hansika Weerasena, Aruna Jayasena, Christina Boucher, Prabhat Mishra

Abstract read

In one paragraph

Article in Briefings in bioinformatics, 2025. The graph could read no effect estimate from its abstract, so it casts no vote on the map. Not yet cited in PubMed.

0numbers the graph read from it

0cells of the map it votes in

0citing papers in PubMed

–field-weighted citation impact

1 · What the graph read from it

What it found

Each row is one number read from the abstract, on the scale the paper reported it, with its interval. Left of the dashed line favours the treatment, right favours the comparator. Under each row is the sentence it came from. New to these charts? A ten-minute tutorial.

The abstract states no effect estimate the extractor could read, or names no intervention and outcome on the map, so this paper lights no cell and moves no belief. It is still indexed, cited and linked below.

2 · The registry

The trial behind it

Trials whose registry record cites this paper, or whose number appears in the abstract. A trial that started after this paper was published is citing it as background, not reporting it.

Neither the registry nor the abstract names a trial number. If this is a trial report, that itself is worth knowing.

3 · Its place in the literature

Who cites it

0 citing papers in PubMed.

No citing paper in PubMed yet.

4 · The record

Corrections and comments

PubMed lists nothing against this paper. Absence here is not a guarantee, only a check that was made.

5 · Who and what money

Authors and funding

4 authors.

Hansika WeerasenaCISE Department, University of Florida, 1889 Museum Road, Gainesville, FL 32611, United States.ORCID 0000-0001-7107-8137

Aruna JayasenaCISE Department, University of Florida, 1889 Museum Road, Gainesville, FL 32611, United States.ORCID 0000-0002-8347-5065

Christina BoucherCISE Department, University of Florida, 1889 Museum Road, Gainesville, FL 32611, United States.ORCID 0000-0001-9509-9725

Prabhat MishraCISE Department, University of Florida, 1889 Museum Road, Gainesville, FL 32611, United States.ORCID 0000-0003-3653-6221

Funding

No grant is acknowledged in the PubMed record.

6 · The paper itself

Abstract

While there is explosive growth in the creation of biological data, researchers rely on ad hoc verification methods such as testing with small simulated datasets. Due to their importance in biology and biomedicine, there is a critical need to verify these algorithms as well as their implementations to ensure that the results and conclusions are trustworthy. In this paper, we explore an effective combination of model checking and theorem proving of bioinformatics software, including BiopLib, BWA, Jellyfish, SDSL, Dashing, SPAdes, and MUMmer. We provide results for model checking for bioinfomatics software libraries and theorem proving for specific properties. Our model checking framework found several potential flaws in the two tools (BiopLib and BWA). We have also detected several failing cases in Succinct Data Structures Library (SDSL).

Indexed as

Computational BiologySoftwareAlgorithmsHumansBurrows–Wheeler transformformal verificationmodel checkingpattern matchingpositional Burrows–Wheeler transformproperty checkingsuccinct data structurestheorem proving

Identifiers

PMID40753536

DOI10.1093/bib/bbaf383

PMCPMC12318479

What OpenQuestion holds

Textmetadata

LicenceCC BY-NC

Read underepoch 390

Registered trials

None linked

Read under generation 80e0d062 · epoch 390. Bibliography from PubMed, PubMed Central and OpenAlex; grants from NIH RePORTER; trial links from ClinicalTrials.gov; estimates, votes and beliefs from the OpenQuestion graph.