Search research articles

ABOUT JoVE

Overview Leadership Blog JoVE Help Center

AUTHORS

Publishing Process Editorial Board Scope & Policies Peer Review FAQ Submit

LIBRARIANS

Testimonials Subscriptions Access Resources Library Advisory Board FAQ

RESEARCH

JoVE Journal Methods Collections JoVE Encyclopedia of Experiments Archive

EDUCATION

JoVE Core JoVE Business JoVE Science Education JoVE Lab Manual Faculty Resource Center Faculty Site

Terms & Conditions of Use

Related Concept Videos

Improving Translational Accuracy

Improving Translational Accuracy

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...

Synthetic Biology

Synthetic Biology

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...

Mechanistic Models: Compartment Models in Algorithms for Numerical Problem Solving

Mechanistic Models: Compartment Models in Algorithms for Numerical Problem Solving

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...

Genome Annotation and Assembly

Genome Annotation and Assembly

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.

Protein Folding Quality Check in the RER

Protein Folding Quality Check in the RER

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...

Molecular Models

Molecular Models

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.

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by

Same author

RAmpSim: a thermodynamic simulator for hybridization capture in metagenomic sequencing.

Bioinformatics (Oxford, England)·2026

Same author

Primer Design through Submodular Function Estimation.

Bioinformatics (Oxford, England)·2026

Same author

Accelerating String Comparison in RLZ Compressed Sequences via LCE Jumps.

bioRxiv : the preprint server for biology·2026

Same author

Building genomic data structures from compressed representations using prefix-free parsing.

Genome research·2026

Same author

RAmpSim: A Thermodynamic Simulator for Hybridization Capture in Metagenomic Sequencing.

bioRxiv : the preprint server for biology·2025

Same author

Toward security-aware portable sequencing.

Nature communications·2025

Search research articles

Related Experiment Video

Updated: Sep 8, 2025

A Web Tool for Generating High Quality Machine-readable Biological Pathways

A Web Tool for Generating High Quality Machine-readable Biological Pathways

Published on: February 8, 2017

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

Hansika Weerasena¹, Aruna Jayasena¹, Christina Boucher¹

¹CISE 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).

Keywords:

Burrows–Wheeler transform formal verification model checking pattern matching positional Burrows–Wheeler transform property checking succinct data structures theorem proving

More Related Videos

Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly

Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly

Published on: April 25, 2016

Integration of Bioinformatics Approaches and Experimental Validations to Understand the Role of Notch Signaling in Ovarian Cancer

Integration of Bioinformatics Approaches and Experimental Validations to Understand the Role of Notch Signaling in Ovarian Cancer

Published on: January 12, 2020

Related Experiment Videos

Last Updated: Sep 8, 2025

A Web Tool for Generating High Quality Machine-readable Biological Pathways

A Web Tool for Generating High Quality Machine-readable Biological Pathways

Published on: February 8, 2017

Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly

Rapid Verification of Terminators Using the pGR-Blue Plasmid and Golden Gate Assembly

Published on: April 25, 2016

Integration of Bioinformatics Approaches and Experimental Validations to Understand the Role of Notch Signaling in Ovarian Cancer

Integration of Bioinformatics Approaches and Experimental Validations to Understand the Role of Notch Signaling in Ovarian Cancer

Published on: January 12, 2020

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.