Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Cache-a-lot: Pushing the Limits of Unsatisfiable Core Reuse in SMT-Based Program Analysis

Rustam Sadykov, Azat Abdullin, Marat Akhin

TL;DR

Cache-a-lot addresses the high cost of SMT solver invocations in program analysis by extending unsat-core reuse through systematic variable substitutions, moving beyond reliance on formula canonization. The method introduces a two-stage pipeline (candidate selection via hash footprints and Bloom filters, followed by substitution collection and joining) to determine if a complete substitution σ exists such that σ(s) ⊆ F, enabling unsat detection without new solver calls. Empirical results on two benchmark families show substantial gains, especially for complex formulas, with up to 74% unsat-core reuse and meaningful time savings, while remaining solver-agnostic and not requiring preprocessing. The work also analyzes canonization effects, memory behavior, and optimisation impacts, concluding that broad substitution-based reuse significantly improves SMT-based program analysis performance and that Cache-a-lot's approach is robust across benchmarks and adaptable to incremental settings in the future.

Abstract

Satisfiability Modulo Theories (SMT) solvers are integral to program analysis techniques like concolic and symbolic execution, where they help assess the satisfiability of logical formulae to explore execution paths of the program under test. However, frequent solver invocations are still the main performance bottleneck of these techniques. One way to mitigate this challenge is through optimizations such as caching and reusing solver results. While current methods typically focus on reusing results from fully equivalent or closely related formulas, they often miss broader opportunities for reuse. In this paper, we propose a novel approach, Cache-a-lot, that extends the reuse of unsatisfiable (unsat) results by systematically considering all possible variable substitutions. This enables more extensive reuse of results, thereby reducing the number of SMT solver invocations and improving the overall efficiency of concolic and symbolic execution. Our evaluation, conducted against the state-of-the-art Utopia solution using two benchmark sets, shows significant improvements, particularly with more complex formulas. Our method achieves up to 74% unsat core reuse, compared to Utopia's 41%, and significant increase in the time savings. These results demonstrate that, despite the additional computational complexity, the broader reuse of unsat results significantly enhances performance, offering valuable advancements for formal verification and program analysis.

Cache-a-lot: Pushing the Limits of Unsatisfiable Core Reuse in SMT-Based Program Analysis

TL;DR

Cache-a-lot addresses the high cost of SMT solver invocations in program analysis by extending unsat-core reuse through systematic variable substitutions, moving beyond reliance on formula canonization. The method introduces a two-stage pipeline (candidate selection via hash footprints and Bloom filters, followed by substitution collection and joining) to determine if a complete substitution σ exists such that σ(s) ⊆ F, enabling unsat detection without new solver calls. Empirical results on two benchmark families show substantial gains, especially for complex formulas, with up to 74% unsat-core reuse and meaningful time savings, while remaining solver-agnostic and not requiring preprocessing. The work also analyzes canonization effects, memory behavior, and optimisation impacts, concluding that broad substitution-based reuse significantly improves SMT-based program analysis performance and that Cache-a-lot's approach is robust across benchmarks and adaptable to incremental settings in the future.

Abstract

Satisfiability Modulo Theories (SMT) solvers are integral to program analysis techniques like concolic and symbolic execution, where they help assess the satisfiability of logical formulae to explore execution paths of the program under test. However, frequent solver invocations are still the main performance bottleneck of these techniques. One way to mitigate this challenge is through optimizations such as caching and reusing solver results. While current methods typically focus on reusing results from fully equivalent or closely related formulas, they often miss broader opportunities for reuse. In this paper, we propose a novel approach, Cache-a-lot, that extends the reuse of unsatisfiable (unsat) results by systematically considering all possible variable substitutions. This enables more extensive reuse of results, thereby reducing the number of SMT solver invocations and improving the overall efficiency of concolic and symbolic execution. Our evaluation, conducted against the state-of-the-art Utopia solution using two benchmark sets, shows significant improvements, particularly with more complex formulas. Our method achieves up to 74% unsat core reuse, compared to Utopia's 41%, and significant increase in the time savings. These results demonstrate that, despite the additional computational complexity, the broader reuse of unsat results significantly enhances performance, offering valuable advancements for formal verification and program analysis.

Paper Structure

This paper contains 28 sections, 3 equations, 10 figures, 5 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Reusing Unsatisfiable Cores of Formulae
  3. Motivating Example
  4. Main Properties
  5. Related Work
  6. Cache-a-lot Approach
  7. Candidate Selection
  8. Hash Footprint
  9. Bloom Filter
  10. Candidate Testing
  11. The Idea
  12. Substitution Collection
  13. Substitution Joining
  14. Optimisations
  15. Implementation Details
  16. ...and 13 more sections

Figures (10)

  • Figure 1: Pipeline of the SMT Formula Reuse Process: The flowchart illustrates the steps involved in reusing unsat cores, beginning with candidate selection using a Bloom filter and proceeding to candidate testing by collection and joining unifying variable substitutions.
  • Figure 2: Table representation of the set of unifying substitutions
  • Figure 3: Join operation on two sets of unifying substitutions
  • Figure 4: Join operation between a partial and unifying substitutions
  • Figure 5: Boxplot of Utopia and Cache-a-lot reuse ratio's
  • ...and 5 more figures