Related Experiment Video
Updated: Sep 8, 2025
08:01
A Web Tool for Generating High Quality Machine-readable Biological Pathways
Published on: February 8, 2017
17.8K
Formal verification of bioinformatics software using model checking and theorem proving.
Hansika Weerasena1, Aruna Jayasena1, Christina Boucher1
1CISE Department, University of Florida, 1889 Museum Road, Gainesville, FL 32611, United States.
Briefings in Bioinformatics
|August 3, 2025
Summary
Researchers need reliable bioinformatics tools. This study uses model checking and theorem proving to verify software, finding flaws in BiopLib, BWA, and Succinct Data Structures Library (SDSL).
Area of Science:
- Bioinformatics
- Computational Biology
- Software Verification
Background:
- Explosive growth in biological data necessitates reliable analysis tools.
- Current verification methods for bioinformatics software are often ad hoc.
- Ensuring the trustworthiness of bioinformatics algorithms and implementations is critical for biology and biomedicine.
Purpose of the Study:
- To explore an effective combination of model checking and theorem proving for bioinformatics software.
- To verify the correctness and reliability of key bioinformatics tools.
- To address the critical need for robust verification in biological data analysis.
Main Methods:
- Applied model checking to bioinformatics software libraries.
- Utilized theorem proving for specific software properties.
- Tested tools including BiopLib, BWA, Jellyfish, SDSL, Dashing, SPAdes, and MUMmer.
Main Results:
- Identified potential flaws in BiopLib and BWA using model checking.
- Detected several failing cases in the Succinct Data Structures Library (SDSL).
- Provided verification results for multiple bioinformatics software packages.
Conclusions:
- Model checking and theorem proving offer effective verification strategies for bioinformatics software.
- The implemented framework successfully uncovered defects in widely used tools.
- Improved verification methods are essential for trustworthy biological research.
Keywords:
Burrows–Wheeler transformformal verificationmodel checkingpattern matchingpositional Burrows–Wheeler transformproperty checkingsuccinct data structurestheorem provingMore Related Videos
Related Concept Videos
02:07Improving Translational Accuracy
11.8K
Base complementarity between the three base pairs of mRNA codon and the tRNA anticodon is not a failsafe mechanism. Inaccuracies can range from a single mismatch to no correct base pairing at all. The free energy difference between the correct and nearly correct base pairs can be as small as 3 kcal/ mol. With complementarity being the only proofreading step, the estimated error frequency would be one wrong amino acid in every 100 amino acids incorporated. However, error frequencies observed in...
11.8K
02:55Synthetic Biology
4.9K
Synthetic biology is an interdisciplinary science that involves using principles from disciplines such as engineering, molecular biology, cell biology, and systems biology. It involves remodeling existing organisms from nature or constructing completely new synthetic organisms for applications such as protein or enzyme production, bioremediation, value-added macromolecule production, and the addition of desirable traits to crops, to name a few.
Golden rice
Golden rice is a genetically modified...
Golden rice
Golden rice is a genetically modified...
4.9K
01:29Mechanistic Models: Compartment Models in Algorithms for Numerical Problem Solving
100
Mechanistic models play a crucial role in algorithms for numerical problem-solving, particularly in nonlinear mixed effects modeling (NMEM). These models aim to minimize specific objective functions by evaluating various parameter estimates, leading to the development of systematic algorithms. In some cases, linearization techniques approximate the model using linear equations.
In individual population analyses, different algorithms are employed, such as Cauchy's method, which uses a...
In individual population analyses, different algorithms are employed, such as Cauchy's method, which uses a...
100
03:36Genome Annotation and Assembly
19.3K
The genome refers to all of the genetic material in an organism. It can range from a few million base pairs in microbial cells to several billion base pairs in many eukaryotic organisms. Genome assembly refers to the process of taking the DNA sequencing data and putting it all back together in a correct order to create a close representation of the original genome. This is followed by the identification of functional elements on the newly assembled genome, a process called genome annotation.
19.3K
01:29Protein Folding Quality Check in the RER
3.8K
ER is the primary site for the maturation and folding of soluble and transmembrane secretory proteins. The calnexin cycle is a specific chaperone system that folds and assesses the confirmation of N-glycosylated proteins before they can exit the ER lumen. The primary players of this quality check pipeline are the lectins, ER-resident chaperones, and a glucosyl transferase enzyme. In case the calnexin system in the lumen fails to salvage a misfolded protein, it is transported to the cytoplasm...
3.8K
02:00Molecular Models
40.3K
Physical models representing molecular architectures of chemical compounds play essential roles in understanding chemistry. The use of molecular models makes it easier to visualize the structures and shapes of atoms and molecules.
40.3K