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

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). [ABSTRACT FROM AUTHOR]

Copyright of Briefings in Bioinformatics is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)