Pending Constraints in Symbolic Execution for Better Exploration and Seeding
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.
Tue 22 SepDisplayed time zone: (UTC) Coordinated Universal Time change
08:00 - 09:00
|Pending Constraints in Symbolic Execution for Better Exploration and Seeding|
Timotej Kapus Imperial College London, UK, Frank Busse Imperial College London, Cristian Cadar Imperial College London, UKPre-print Media Attached
|Broadening Horizons of Multilingual Static Analysis: Semantic Summary Extraction from C Code for JNI Program Analysis|
|Assessing and Restoring Reproducibility of Jupyter Notebooks|