一句话：在 CPAchecker 中实现基于抽象与 CEGAR 的符号执行，自动识别符号事实以缓解路径爆炸并判定可达性。
符号执行在验证中常受路径爆炸困扰。本文提出 CPA-SymExec，一个实现在开源可配置验证框架 CPAchecker 中的符号执行工具。它基于抽象与反例引导的抽象精化（CEGAR），并利用约束插值自动检测需要跟踪的符号事实，从而只保留判定目标程序区域可达性所必需的小规模约束集。作者将 CPA-SymExec 与当前最优的、基于 KLEE 的符号执行引擎 Symbiotic 以及 KLEE 本身进行性能对比，实验涵盖两类分析任务：寻找到达特定位置的可执行路径（如获取测试向量），以及确认不存在到达该位置的路径。结果表明，相比无抽象的符号执行，该实现能更好地缓解路径爆炸问题。工具以 Apache 2 许可证发布，源码与演示视频均可公开获取。
We present CPA-SymExec, a tool for symbolic execution that is implemented in the open-source, configurable verification framework CPAchecker. Our implementation automatically detects which symbolic facts to track, in order to obtain a small set of constraints that are necessary to decide reachability of a program area of interest. CPA-SymExec is based on abstraction and counterexample-guided abstraction refinement (CEGAR), and uses a constraint-interpolation approach to detect symbolic facts. We show that our implementation can better mitigate the path-explosion problem than symbolic execution without abstraction, by comparing the performance to the state-of-the-art Klee-based symbolic-execution engine Symbiotic and to Klee itself. For the experiments we use two kinds of analysis tasks: one for finding an executable path to a specific location of interest (e.g., if a test vector is desired to show that a certain behavior occurs), and one for confirming that no executable path to a specific location exists (e.g., if it is desired to show that a certain behavior never occurs). CPA-SymExec is released under the Apache 2 license and available (inclusive source code) at https://cpachecker.sosy-lab.org. A demonstration video is available at https://youtu.be/qoBHtvPKtnw.
DOI 原文 ·
@inproceedings{paperbot4772,
title = {CPA-SymExec: efficient symbolic execution in CPAchecker},
author = {Dirk Beyer and Thomas Lemberger},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3240478}
}