RSTDResearch on Scientific and Technological Development3070-07013070-0728Art and Technology10.61369/RSTD.2026020002Article基于Frama-C的Select算法C 源码的形式化验证https://artdesignp.com/journal/RSTD/1/2/10.61369/RSTD.2026020002姜雨函2026122026-02-20本文针对Select算法C源码实现的逻辑正确性和运行可靠性提出了一种形式化验证方法，该方法通过Frama-C形式化验证工具及其配套插件的相互协作，并采用ACSL规范语言对Select算法的C源码需满足的核心属性进行标注，旨在对该算法形成清晰的形式化表达，最后基于抽象解释与定理证明技术完成严谨的验证推理，以确保算法实现与预设规范的一致性.通过此方法可以证明Select算法的C源码的逻辑正确性以及运行可靠性，从而解决该算法在常规手工测试中因穷举情况覆盖不完整而造成的隐性缺陷逃逸和效率低下问题。Frama-C,Select算法,形式化验证

[1] 侯潇逸, 田杰斌, 赵硕, 等. 基于多头注意力机制的相似源码漏洞检测仿真[J].计算机仿真,2025,42(11):242-247.[2] 马佳鑫, 张铮, 刘鹏, 等. 基于反向数据流传播的SQL 语句随机化[J].计算机应用研究,2025,42(10):3106-3113.[3] 王帅, 黄晨, 江云松, 等.AFL-VTest:航天嵌入式软件模糊测试框架[J].计算机科学,2025,52(12):9-17.[4] 崔少轩, 喻垚慎. 静态程序分析过程中形式化验证工具Frama-C的应用[J]. 计算技术与自动化, 2019,38(01):114-117.[5] 包晟宏, 姚有健, 李小丫, 等. 集成式PU学习方法PUEVD及其在软件源码漏洞检测中的应用[J].计算机科学,2025,52(S1):865-873.[6] 张元, 熊风光, 杨晓文, 等. 处理机调度实验系统开发及实验案例设计[J].工业和信息化教育,2025,(03):84-89.[7]付俊仪, 张倩颖, 王国辉, 等. TrustZone中断隔离机制的形式化验证[J]. 小型微型计算机系统, 2023, 44(09):2105-2112.[8] 郭肖旺, 赵德政. 基于NuSMV 的LD 和ST语言形式化验证研究与实现[J]. 电子技术应用, 2022, 48(12):94-99.[9] 钱汉伟, 王承毅. 操作系统形式化验证综述[J]. 河海大学学报( 自然科学版), 2021, 49(05):473-481.[10] 罗娟, 王燕芩. 形式化方法应用于计算机联锁软件的安全验证研究[J]. 铁路计算机应用, 2016, 25(11):53-57.