量化形式化验证中 SMT 求解器的不稳定性

AI 摘要

该论文研究形式化验证中 SMT 求解器的不稳定性问题，即语义等价的查询排列会导致求解时间大幅波动甚至超时。作者使用变异系数（CV）对来自三个软件领域的 60,000 个 SMT 查询进行量化分析，发现不稳定性在各领域均显著存在，且平均求解时间越长的查询越不稳定。研究进一步提出，若优化查询结构以降低运行时间而非方差，可在缓解不稳定性的同时提升求解器整体性能。

正文节选

Quantifying SMT Solver Instability for Formal Verification Abstract Program verification has become commonplace in software development projects, and much of its feasibility can be attributed to the potential of SMT solvers to automate model checking and other verification techniques. However, SMT instability, a phenomenon where semantically equivalent permutations of source code take much longer to solve or timeout, has been found to interrupt workflows and make software engineers more likely t

发布时间：2026-10-12 12:00

抓取时间：2026-10-12 12:24

来源机构：arXiv