paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Automatically testing string solvers

自动测试字符串求解器
ICSE Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering2020匹配度 3/10 · 论文关注字符串 SMT 求解器的自动测试与不健全性检测，属于形式化方法与约束求解器可靠性方向；但用户当前核心兴趣集中在 LLM/Agent 与静态分析/形式化验证的交叉、浮点程序分析及贝叶斯程序分析，该论文未涉及这些交叉方向或 LLM/Agent 方法。引用 28 inbox
Alexandra Bugariu, Peter Müller
测试、调试与修复逻辑与约束编程
crossref: 2026-09-12

AI 速览

一句话：针对字符串 SMT 求解器难以可靠检测不健全性的问题，提出自动测试方法以暴露其错误答案。

SMT 求解器广泛应用于程序验证、程序合成和测试用例生成，其结果正确性至关重要。然而，这类求解器是复杂且高度优化的软件系统，确保其正确性十分困难；现有最先进的测试技术无法可靠检测求解器何时是不健全的（unsound）。本文聚焦字符串求解器的自动测试，旨在通过自动化手段发现求解器返回错误答案的情况。标题与摘要表明该工作属于面向 SMT 求解器的测试方法研究，强调不健全性检测这一挑战；摘要未给出具体技术细节与实验结果。

问题
SMT 求解器（尤其是字符串求解器）复杂且高度优化，现有测试技术难以可靠检测其不健全性，而程序验证等应用依赖其正确性。
方法
论文提出自动测试字符串求解器的方法，目标是自动发现求解器的 unsoundness；摘要未展开具体测试机制。
评估
摘要未给出评估方式的具体信息；从问题设定看，评估应围绕自动检测字符串求解器的错误答案或不健全性展开。
原文摘要（Abstract）

SMT solvers are at the basis of many applications, such as program verification, program synthesis, and test case generation. For all these applications to provide reliable results, SMT solvers must answer queries correctly. However, since they are complex, highly-optimized software systems, ensuring their correctness is challenging. In particular, state-of-the-art testing techniques do not reliably detect when an SMT solver is unsound.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot5594,
  title = {Automatically testing string solvers},
  author = {Alexandra Bugariu and Peter Müller},
  booktitle = {ICSE},
  year = {2020},
  doi = {10.1145/3377811.3380398}
}