NRB 验证逻辑的可靠性与完备性
计算机科学中的逻辑
2018-09-06 v2
摘要
这篇短文给出了用于确定性命令式程序的 NRB 验证逻辑的模型及其完备性证明，该逻辑过去曾被用作对大型、快速变化的开源 C 代码档案（如 Linux 内核源码）进行自动语义检查的基础。该模型是一个彩色状态转移模型，从上方近似程序可能的转移集合。相应地，该逻辑能够捕捉所有可能在程序特定点触发特定缺陷的轨迹，但也可能会标记误报。
引用
@article{arxiv.1306.5585,
title = {Soundness and Completeness of the NRB Verification Logic},
author = {Peter T. Breuer and Simon J. Pickin},
journal= {arXiv preprint arXiv:1306.5585},
year = {2018}
}
备注
To appear in OpenCert 2013 Workshop, Sept 23, Madrid, 15p