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

PDF DOI KLEE-Float Aachen KLEE-Float London Benchmarks Aachen Benchmarks Aachen
bibtex
@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.

Awards