Unsatisfiable Core Guided Constraint Solving in Symbolic Execution

Authors:
Open Access
Publisher website
Google Scholar
Abstract
Constraint solving remains a fundamental challenge in symbolic execution. To reduce the computational overhead of SMT solvers, modern symbolic execution tools commonly cache and reuse the results of previously solved queries. However, existing caching mechanisms primarily focus on satisfiable queries, offering limited support for unsatisfiable ones, which are still delegated to the underlying SMT solver. To address this problem, we introduce a novel Unsatisfiable Core Guided ( Ucg ) constraint solving framework for symbolic execution. The proposed framework accelerates constraint solving by systematically exploiting unsatisfiable cores, which provide compact explanations for unsatisfiability. Specifically, Ucg first constructs an unsatisfiable core cache with a least-recently-used (LRU) replacement policy to enable the reuse of previously computed unsatisfiable cores. Upon a cache miss, Ucg further exploits the temporal locality of assertions within unsatisfiable cores to predict a potential unsatisfiable core for the pending query. This predicted core serves as an over-approximation of the original query and is likely to be unsatisfiable. By solving this much smaller over-approximated formula, Ucg can infer the satisfiability of the original query with substantially reduced SMT solver effort. We integrated Ucg into Klee , a state-of-the-art symbolic execution tool for C programs. Experimental results on 99 open-source real-world programs demonstrate that Ucg consistently improves the efficiency of both constraint solving and path exploration in symbolic execution across various search strategies. In the best-case scenario, Ucg can achieve improvements of up to two orders of magnitude.

This publication has 60 references indexed in Scilit: