An extension to the KLEE symbolic execution engine that supports reasoning about floating-point arithmetic and a benchmark set used to evaluate the tool.

Overview

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 our 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.

Download

See the instructions on how to build the tools and the benchmarks.

Research Support

This research is supported by EPSRC through a CASE studentship (sponsored by ARM) and two EPSRC Early Career Fellowships (EP/L002795/1 and EP/N026314/1); and by the European Research Council (ERC) under the EU’s Horizon 2020 Research and Innovation Programme (grant agreement n.~647295 (SYMBIOSYS)).

Publications

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

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

    IEEE/ACM International conference on Automated Software Engineering (ASE 2017)