paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Finding and Understanding Incompleteness Bugs in SMT Solvers

发现并理解 SMT 求解器中的不完备性缺陷
ASE Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering2022匹配度 3/10 · 论文研究 SMT 求解器不完备性缺陷的变异测试，属于形式化验证/约束求解基础设施测试；与用户关注的 LLM/Agent 改进静态分析、浮点程序分析、贝叶斯程序分析及 Agentic 程序分析没有直接交叉，仅因 SMT 是静态分析与形式化验证的基础设施而弱相关。引用 5 inbox
Mauro Bringolf, Dominik Winterer, Zhendong Su
测试、调试与修复逻辑与约束编程
crossref: 2026-09-12

AI 速览

一句话：提出 Janus，用保持可满足性的变异测试 SMT 求解器，发现并理解返回 unknown 的不完备性缺陷。

SMT 求解器有时会对输入意外返回 unknown，形成不完备性缺陷，影响求解可靠性却缺乏系统检测手段。本文提出 Janus，核心洞察是对种子 SMT 公式应用保持可满足性的局部弱化与强化规则进行变异，生成测试用例以暴露求解器的不完备性。Janus 构建在 SMT 求解器模糊测试框架 YinYang 之上。作者于 2021 年 6 月至 8 月对 Z3 和 CVC5 进行压力测试，共报告 31 个不完备性缺陷，其中 26 个被确认为唯一缺陷，19 个已被开发者修复。这些缺陷涵盖功能性、回归性和性能问题，并引发开发者深入分析讨论。

问题
SMT 求解器可能对某些输入意外返回 unknown，形成不完备性缺陷；现有测试方法难以有效发现并理解此类缺陷。
方法
Janus 对种子 SMT 公式应用保持可满足性的局部弱化与强化规则进行变异，并在 SMT 求解器模糊测试框架 YinYang 上实现，用于测试求解器。
评估
在 Z3 和 CVC5 上从 2021 年 6 月到 8 月进行压力测试，报告 31 个不完备性缺陷，其中 26 个确认为唯一缺陷、19 个已修复，涵盖功能性、回归性和性能问题。
原文摘要（Abstract）

We propose Janus, an approach for finding incompleteness bugs in SMT solvers. The key insight is to mutate SMT formulas with local weakening and strengthening rules that preserve the satisfiability of the seed formula. The generated mutants are used to test SMT solvers for incompleteness bugs, i.e., inputs on which SMT solvers unexpectedly return unknown. We realized Janus on top of the SMT solver fuzzing framework YinYang. From June to August 2021, we stress-tested the two state-of-the-art SMT solvers Z3 and CVC5 with Janus and totally reported 31 incompleteness bugs. Out of these, 26 have been confirmed as unique bugs and 19 are already fixed by the developers. Our diverse bug findings uncovered functional, regression, and performance bugs—several triggered discussions among the developers sharing their in-depth analysis.

链接与引用

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

BibTeX 
@inproceedings{paperbot7169,
  title = {Finding and Understanding Incompleteness Bugs in SMT Solvers},
  author = {Mauro Bringolf and Dominik Winterer and Zhendong Su},
  booktitle = {ASE},
  year = {2022},
  doi = {10.1145/3551349.3560435}
}