PG-KLEE: Trading Soundness for Coverage

Abstract

Comprehensive test inputs are an essential ingredient for dynamic software analysis techniques, yet are typically impossible to obtain and maintain. Automated input generation techniques can supplant manual effort in many contexts, but they also exhibit inherent limitations in practical applications. Therefore, the best approach to input generation for a given application task necessarily entails compromise. Most symbolic execution approaches maintain soundness by sacrificing completeness. In this paper, we take the opposite approach and demonstrate PG-KLEE, an input generation tool that over-approximates program behavior to achieve complete coverage. We also summarize some empirical results that validate our claims. Our technique is detailed in an earlier paper [16], and the source code of PG-KLEE is available from [2].Video URL: Https://youtu.be/b1ajzW6YWds