paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Combining static analysis error traces with dynamic symbolic execution (experience paper)

结合静态分析错误轨迹与动态符号执行（经验论文）
ISSTA Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis2022匹配度 4/10 · 论文属于静态分析与动态符号执行的结合，聚焦告警确认与触发输入生成，与程序分析、工业落地和问题驱动的研究偏好有一定交集；但未涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析，因此不匹配用户当前追踪的核心交叉方向。引用 16 inbox
Frank Busse, Pritam Gharat, Cristian Cadar, Alastair F. Donaldson
程序分析与抽象解释测试、调试与修复
crossref: 2026-09-12

AI 速览

一句话：提出结合静态分析错误轨迹与动态符号执行的技术，用轨迹引导搜索并剪枝，快速确认告警并生成触发输入。

静态分析工具常产生大量告警，人工甄别成本高。本文报告一种经验性技术：当静态分析给出程序的部分错误轨迹，并为轨迹各步标注其认为对触发缺陷重要的条件时，动态符号执行可加以利用。方法将搜索启发式地导向最贴近静态轨迹的路径，并利用各步条件剪枝搜索空间。若告警为真阳性，该策略有望快速确认缺陷并生成触发输入。论文以经验报告形式描述实现过程与观察，重点在于静态分析与动态符号执行的协同，而非全新理论。

问题
静态分析报告数量多且常含误报，如何高效甄别并确认告警是实际问题。
方法
利用静态分析给出的部分错误轨迹及其标注条件，引导动态符号执行的路径探索并剪枝搜索空间，从而优先确认可能的真阳性并生成触发输入。
评估
论文以经验报告形式实现并讨论该技术；摘要未报告量化评估结果，评估目标是快速确认缺陷并产出触发输入。
原文摘要（Abstract）

This paper reports on our experience implementing a technique for sifting through static analysis reports using dynamic symbolic execution. Our insight is that if a static analysis tool produces a partial trace through the program under analysis, annotated with conditions that the analyser believes are important for the bug to trigger, then a dynamic symbolic execution tool may be able to exploit the trace by (a) guiding the search heuristically so that paths that follow the trace most closely are prioritised for exploration, and (b) pruning the search using the conditions associated with each step of the trace. This may allow the bug to be quickly confirmed using dynamic symbolic execution, if it turns out to be a true positive, yielding an input that triggers the bug.

链接与引用

DOI 原文 ·

BibTeX 
@inproceedings{paperbot7378,
  title = {Combining static analysis error traces with dynamic symbolic execution (experience paper)},
  author = {Frank Busse and Pritam Gharat and Cristian Cadar and Alastair F. Donaldson},
  booktitle = {ISSTA},
  year = {2022},
  doi = {10.1145/3533767.3534384}
}