SMT求解器中浮点性能问题的蜕变测试
Metamorphic Testing for Floating-Point Performance Issues in SMT Solvers
浏览论文内容
中文总结 AI 辅助
本文提出一种基于语义保持重写规则的蜕变测试方法，针对SMT求解器浮点公式处理中的性能问题，在真实输入下发现简化后求解时间显著增加，最高达33.4倍。
中文摘要 AI 辅助
SMT求解器在程序验证和综合等多个领域至关重要。尽管其正确性和性能已被广泛研究，但浮点理论的性能测试仍然有限，尤其是针对真实世界查询。我们提出了一种蜕变测试方法，利用语义保持的重写规则，聚焦于浮点特殊值和窥孔优化，以揭示SMT求解器处理浮点公式时的有意义性能问题。使用真实世界测试输入，我们的方法能够为每个测试的求解器识别出SMT查询，在这些查询被简化时求解时间增加；我们观察到Z3的减速高达33.4倍，MathSAT为5.6倍，cvc5为4.5倍，Bitwuzla为1.8倍。我们进一步观察到，当使用从语法随机生成的输入文件时，该方法效果较差。
英文摘要
SMT solvers are essential in various domains, including program verification and synthesis. Although their correctness and performance have been extensively studied, performance testing for the floating-point theory remains limited, particularly for real-world queries. We propose a metamorphic testing approach that uses semantics-preserving rewrite rules, focusing on floating-point special values and peep-hole optimizations, to uncover meaningful performance issues in SMT solvers' handling of floating-point formulas. Using real-world test inputs, our approach is able to identify for every solver tested SMT queries for which solving time increases when the queries are simplified; we see slowdowns of up to 33.4x for Z3, 5.6x for MathSAT, 4.5x for cvc5, and 1.8x for Bitwuzla. We further observe that the approach is less successful when using input files that were randomly generated from a grammar.
发表机构
- MPI-SWS（马克斯·普朗克软件系统研究所）
- Uppsala University（乌普萨拉大学）
机构由 AI 辅助整理，请以论文原文为准。
