一句话：首个内存安全验证中单元证明的实证研究，提出系统化构建方法并评估其效果与成本。
内存安全缺陷严重威胁软件可靠性，组织常采用组合有界模型检验（BMC），以单元证明形式化验证内存安全。但单元证明的创建方法缺乏系统性，跨组织与项目内均不一致，易导致错误与漏报。本文开展首个内存安全验证中单元证明的实证研究，提出利用验证反馈与客观标准的系统化构建方法，为四个嵌入式操作系统开发73个单元证明，并评估其有效性、特征、成本与泛化性。结果显示：单元证明具成本效益，可检测74%的重现缺陷，提高BMC边界后额外发现9%，并暴露20个新缺陷；嵌入式软件所需证明较小，平均开发87分钟、执行61秒。研究为工程实践与工具设计提供指导与实证依据。
Memory safety defects pose a major threat to software reliability, enabling cyberattacks, outages, and crashes. To mitigate these risks, organizations adopt Compositional Bounded Model Checking (BMC), using unit proofs to formally verify memory safety. However, methods for creating unit proofs vary across organizations and are inconsistent within the same project, leading to errors and missed defects. In addition, unit proofing remains understudied, with no systematic development methods or empirical evaluations. This work presents the first empirical study on unit proofing for memory safety verification. We introduce a systematic method for creating unit proofs that leverages verification feedback and objective criteria. Using this approach, we develop 73 unit proofs for four embedded operating systems and evaluate their effectiveness, characteristics, cost, and generalizability. Our results show unit proofs are cost-effective, detecting 74% of recreated defects, with an additional 9% found with increased BMC bounds, and 20 new defects exposed. We also found that embedded software requires small unit proofs, which can be developed in 87 minutes and executed in 61 seconds on average. These findings provide practical guidance for engineers and empirical data to inform tooling design.
@inproceedings{abs-2503-13762,
title = {Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification},
author = {Paschal C Amusuo and Owen Cochell and Taylor Le Lievre and Parth V Patil and Aravind Machiry and James C Davis},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3744916.3764525}
}