一句话：提出轻量、通用的骨架近似枚举（SAE）技术，用于测试所有一阶理论的 SMT 求解器并发现大量真实缺陷。
SMT 求解器在符号执行、程序验证等领域应用广泛，确保其正确性至关重要。然而现有测试方法成本高，且受测试预言问题限制，难以推广到不同求解器和理论。本文提出骨架近似枚举（SAE），一种面向所有一阶理论的轻量且通用的 SMT 求解器测试技术，用以补充现有方法并克服其不足。作者将 SAE 应用于 Z3 和 CVC4 两个成熟的最先进求解器；截至写作时，共发现 71 个已确认缺陷，其中 55 个已被修复。结果表明该技术对工业级 SMT 求解器具有实用性和缺陷发现能力。
Ensuring the equality of SMT solvers is critical due to its broad spectrum of applications in academia and industry, such as symbolic execution and program verification. Existing approaches to testing SMT solvers are either too costly or find difficulties generalizing to different solvers and theories, due to the test oracle problem. To complement existing approaches and overcome their weaknesses, this paper introduces skeletal approximation enumeration (SAE), a novel lightweight and general testing technique for all first-order theories. To demonstrate its practical utility, we have applied the SAE technique to test Z3 and CVC4, two comprehensively tested, state-of-the-art SMT solvers. By the time of writing, our approach had found 71 confirmed bugs in Z3 and CVC4,55 of which had already been fixed.
DOI 原文 ·
@inproceedings{paperbot6416,
title = {Skeletal approximation enumeration for SMT solver testing},
author = {Peisen Yao and Heqing Huang and Wensheng Tang and Qingkai Shi and Rongxin Wu and Charles Zhang},
booktitle = {FSE},
year = {2021},
doi = {10.1145/3468264.3468540}
}