@inproceedings{liewFloatingPointSymbolicExecution2017,
author = {Liew, Daniel and Schemmel, Daniel and Cadar, Cristian and Donaldson, Alastair F. and Zähl, Rafael and Wehrle, Klaus},
title = {{{Floating-Point}} {{Symbolic}} {{Execution}}: {{A}} {{Case}} {{Study}} in {{N-Version}} {{Programming}}},
booktitle = {{{IEEE/ACM}} {{International}} {{Conference}} on {{Automated}} {{Software}} {{Engineering}} {{(ASE}} 2017)},
location = {Urbana-Champaign, IL, USA},
pages = {601--612},
year = {2017},
doi = {10.1109/ASE.2017.8115670},
}
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.
Our paper was awarded "Best Experience Paper" at ASE 2017.