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

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.

Please click here for more details about this work.

Dan Liew‘s research interests include software verification using symbolic execution and static analysis. He received an MSc in Computing from Imperial College during which he contributed to the KLEE project. Prior to this he studied Physics at the University of Bristol which included an industrial placement with Sharp laboratories of Europe. Daniel’s PhD studies are generously funded by the EPSRC industrial case studentship with ARM.

Joint seminar with the Multicore Programming Group.