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

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.

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

Awards

  • Our paper was awarded “Best Experience Paper” at ASE 2017.
    ASE 2017 Best Experience Paper Award
PhD Student

I am a researcher and head of Systems Analysis at the Chair of Communication and Distributed Systems at RWTH Aachen University, where I research the testability of distributed systems. My specific focus is on the applicability of Symbolic Execution to real world software.

Next
Previous

Related