A variation on standard symbolic execution, where expensive branch feasibility checks are delayed until they are necessary for further exploration of the program.

Overview

Symbolic execution is a well established technique for software testing and analysis. However, scalability continues to be a challenge, both in terms of constraint solving cost and path explosion. In this work, we present a novel approach for symbolic execution, which can enhance its scalability by aggressively prioritizing execution paths that are already known to be feasible, and deferring all other paths. We evaluate our technique on nine applications, including SQLite3, make and tcpdump and show it can achieve higher coverage for both seeded and non-seeded exploration.

Artefact

The artefact page is available here.

Research Support

This research was supported in part by the UK EPSRC via grant EP/N007166/1 and a PhD studentship.

Publications

  • Pending Constraints in Symbolic Execution for Better Exploration and Seeding

    Timotej Kapus, Frank Busse, Cristian Cadar

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

Talks

  • Pending Constraints in Symbolic Execution for Better Exploration and Seeding

    Timotej Kapus

    Talk @ ASE 2020