元编译、切片与符号执行的协同效应
编程语言
2012-01-24 v1
摘要
我们介绍了一种用于发现程序中真实错误的新颖技术。该技术基于三种成熟方法的协同效应:元编译(metacompilation)、切片和符号执行。更具体地说,我们在给定程序中植入代码,以跟踪代表各类错误的状态机运行。接着,我们对程序进行切片以减小其规模,同时不影响状态机的运行。随后,我们对切片后的程序进行符号执行。根据符号执行的类型,该技术既可以作为独立的缺陷查找技术使用,也可以用于剔除另一缺陷查找工具输出中的部分误报。我们提供了若干示例,展示了该技术的实际适用性。
引用
@article{arxiv.1201.4719,
title = {On Synergy of Metal, Slicing, and Symbolic Execution},
author = {Jiří Slabý and Jan Strejček and Marek Trtík},
journal= {arXiv preprint arXiv:1201.4719},
year = {2012}
}