Cache-a-lot：在SMT-based程序分析中推动不可满足核心复用的极限
软件工程
2025-04-11 v1
摘要
满足模理论（SMT）求解器是concolic和符号执行等程序分析技术的核心，他们帮助判断逻辑公式的可满足性以探索受测试程序的执行路径。然而，频繁的求解器调用仍是这些技术的主要性能瓶颈。通过缓存和重用求解结果可缓解这一挑战。虽然现有方法通常 focus on 重用完全等效或 closely related 公式的结果，但常常错失更广泛的复用机会。本文提出一种新方法Cache-a-lot，通过系统性地考虑所有可能的变量替换，扩展了不可满足（unsat）结果的复用，从而减少SMT求解器的调用次数，提高concolic和符号执行的整体效率。我们的评估使用两个基准集针对最先进的Utopia解决方案进行，显示出显著的改进，特别是在更复杂的公式方面。该方法实现了最高达74%的unsat core复用，远高于Utopia的41%，并显著增加时间节省。这些结果表明，尽管增加了计算复杂度，但更广泛的复用不可满足结果显著提升了性能，为形式化验证和程序分析提供了重要的进步。
引用
@article{arxiv.2504.07642,
title = {Cache-a-lot: Pushing the Limits of Unsatisfiable Core Reuse in SMT-Based Program Analysis},
author = {Rustam Sadykov and Azat Abdullin and Marat Akhin},
journal= {arXiv preprint arXiv:2504.07642},
year = {2025}
}