一句话：提出子公式缓存框架并集成到模型计数求解器，利用跨约束共享的子公式显著加速定量程序分析。
定量程序分析（如软件可靠性、定量信息流、侧信道检测与攻击合成）大多依赖模型计数约束求解器，而求解器往往是可扩展性的瓶颈。已有公式缓存虽能加速昂贵的模型计数查询，但只针对整条公式，未能利用程序分析过程中生成的非相同约束之间共享的子公式。本文提出子公式缓存框架，识别并复用这些跨约束的共享子公式，并将其集成进模型计数约束求解器。作者在三个定量程序分析场景下进行评估：符号执行生成的模型计数约束、基于概率符号执行的可靠性分析、以及侧信道的自适应攻击合成。实验结果证明，该子公式缓存方法显著提升了定量程序分析的性能。
Quantitative program analysis is an emerging area with applications to software reliability, quantitative information flow, side-channel detection and attack synthesis. Most quantitative program analysis techniques rely on model counting constraint solvers, which are typically the bottleneck for scalability. Although the effectiveness of formula caching in expediting expensive model-counting queries has been demonstrated in prior work, our key insight is that many subformulas are shared across non-identical constraints generated during program analyses. This has not been utilized by prior formula caching approaches. In this paper we present a subformula caching framework and integrate it into a model counting constraint solver. We experimentally evaluate its effectiveness under three quantitative program analysis scenarios: 1) model counting constraints generated by symbolic execution, 2) reliability analysis using probabilistic symbolic execution, 3) adaptive attack synthesis for side-channels. Our experimental results demonstrate that our subformula caching approach significantly improves the performance of quantitative program analysis.
DOI 原文 ·
@inproceedings{paperbot5184,
title = {Subformula Caching for Model Counting and Quantitative Program Analysis},
author = {William Eiers and Seemanta Saha and Tegan Brennan and Tevfik Bultan},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00050}
}