基于插桩和布尔逻辑的运行时程序验证框架

• 作者: 张颖楠 彭飞 李业华 顾乃杰
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: RPA框架 RPAL语言 运行时程序验证 程序插桩 布尔逻辑 事实推理
• 年，卷（期）: 2013,（1）
• 所属期刊栏目: 专栏
• 页码范围: 29-34,40
• 页数: 7页
• 分类号: TP311
• 字数: 7036字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2013.01.006

摘要

针对软件测试和静态程序验证中存在的连续性程序执行验证和推理问题,提出一个基于程序插桩和布尔逻辑的运行时程序验证框架——RPA.定义一种用于描述运行时程序性质和规范的动态逻辑语言RPAL,实现自动化插桩以收集运行时程序状态信息,设计一个支持高效验证的句子调度算法.实验结果表明,结合合适的谓词扩展,RPA可以有效地验证和分析软件逻辑,发现潜在的软件错误.