Toward More Scalable Symbolic Execution via Code Chopping

Abstract

Dynamic symbolic execution is a program analysis technique that can automatically explore and analyse paths through a program. It is now a key ingredient in many computer science areas, such as software engineering, computer security, and software systems, to name just a few.

For many tasks, such as failure reproduction, coverage augmentation and patch testing, many parts of the code are irrelevant and could be safely skipped. Chopped symbolic execution is a technique that can aggressively skip potentially irrelevant parts of the code, lazily executing paths through them if and only if they are needed later on. In this talk, I will introduce chopped symbolic execution, show how its precision can be improved via a novel past-sensitive pointer analysis, and present promising preliminary results on failure reproduction and coverage augmentation.

The talk is based on joint work with David Trabish, Noam Rinetzky, Timotej Kapus and Andrea Mattavelli.

Keynote at TAPAS workshop.