kirancodes.me
To Proof Maintenance & Beyond!
ASE 2017

Floating-point symbolic execution: a case study in n-version programming

Daniel Liew, Daniel Schemmel, Cristian Cadar, Alastair F. Donaldson, Rafael Zähl, Klaus Wehrle

DOI 10.1109/ase.2017.8115670dblp

Abstract

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.

BibTeX
@inproceedings{Liew-al:ASE17,
  author    = {Daniel Liew and
               Daniel Schemmel and
               Cristian Cadar and
               Alastair F. Donaldson and
               Rafael Z{\"{a}}hl and
               Klaus Wehrle},
  title     = {Floating-point symbolic execution: a case study in n-version programming},
  booktitle = {ASE},
  pages     = {601--612},
  publisher = {{IEEE} Computer Society},
  year      = {2017},
}

Related papers