Floating-Point Symbolic Execution: A Case Study in N-Version Programming

PDF DOI KLEE-Float Aachen KLEE-Float London Benchmarks Aachen Benchmarks Aachen
bibtex
1@inproceedings{liewFloatingPointSymbolicExecution2017,
2  author = {Liew, Daniel and Schemmel, Daniel and Cadar, Cristian and Donaldson, Alastair F. and Zähl, Rafael and Wehrle, Klaus},
3  title = {{{Floating-Point}} {{Symbolic}} {{Execution}}: {{A}} {{Case}} {{Study}} in {{N-Version}} {{Programming}}},
4  booktitle = {{{IEEE/ACM}} {{International}} {{Conference}} on {{Automated}} {{Software}} {{Engineering}} {{(ASE}} 2017)},
5  location = {Urbana-Champaign, IL, USA},
6  pages = {601--612},
7  year = {2017},
8  doi = {10.1109/ASE.2017.8115670},
9}

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.

Awards