Weerasena Hansika, Jayasena Aruna, Boucher Christina, Mishra Prabhat
CISE Department, University of Florida, 1889 Museum Road, Gainesville, FL 32611, United States.
Brief Bioinform. 2025 Jul 2;26(4). doi: 10.1093/bib/bbaf383.
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).
虽然生物数据的创建呈爆炸式增长，但研究人员依赖临时验证方法，如使用小型模拟数据集进行测试。由于这些数据在生物学和生物医学中的重要性，迫切需要验证这些算法及其实现，以确保结果和结论是可信的。在本文中，我们探索了生物信息学软件（包括BiopLib、BWA、Jellyfish、SDSL、Dashing、SPAdes和MUMmer）的模型检查和定理证明的有效结合。我们提供了生物信息学软件库的模型检查结果以及特定属性的定理证明结果。我们的模型检查框架在两个工具（BiopLib和BWA）中发现了几个潜在缺陷。我们还在简洁数据结构库（SDSL）中检测到了几个失败案例。
