Floating-point symbolic execution: A case study in N-version programming
Floating-point symbolic execution: A case study in N-version programming
复制标题
DOI：
10.1109/ase.2017.8115670
复制
发表时间：
2017-10
期刊：
影响因子：
--
通讯作者：
D. Liew;Daniel Schemmel;Cristian Cadar;Alastair F. Donaldson;Rafael Zähl;Klaus Wehrle
中科院分区：
文献类型：
--
作者：
D. Liew;Daniel Schemmel;Cristian Cadar;Alastair F. Donaldson;Rafael Zähl;Klaus Wehrle
符号执行是用于测试软件的众所周知的程序分析技术，它大量使用约束求解器。最近对浮点约束解决方案的支持使得在符号执行工具中支持浮点推理变得可行。在本文中，我们介绍了两个研究团队的经验，这些研究团队独立地为受欢迎的象征性执行引擎Klee添加了浮点支持。由于两个团队独立开发了他们的扩展，因此这创造了难得的机会，可以在这两个实现之间进行严格的比较，这本质上是关于N反编程的现代案例研究。作为比较的一部分，我们报告了每个团队做出的不同设计和实施决策，并显示了它们对严格组装和测试的基准集的影响，本身就是本文的贡献。
Symbolic execution is a well-known program analysis technique for testing software, which makes intensive use of constraint solvers. Recent support for floating-point constraint solving has made it feasible to support floating-point reasoning in symbolic execution tools. In this paper, we present the experience of two research teams that independently added floating-point support to KLEE, a popular symbolic execution engine. Since the two teams independently developed their extensions, this created the rare opportunity to conduct a rigorous comparison between the two implementations, essentially a modern case study on N-version programming. As part of our comparison, we report on the different design and implementation decisions taken by each team, and show their impact on a rigorously assembled and tested set of benchmarks, itself a contribution of the paper.