一句话：提出将 SMT 公式编码为程序并用覆盖率引导模糊测试求解，特别针对浮点约束，实现 JFS 工具。
本文研究用覆盖率引导模糊测试来证明有限变量域上 SMT 公式的可满足性，重点面向浮点约束。方法是将 SMT 公式编码为一个程序，使某个位置可达当且仅当程序输入对应公式的满足赋值；随后用覆盖率引导模糊测试搜索能到达该位置的输入，从而得到满足赋值。作者实现工具 JFS，并开展大规模实验。结果表明，JFS 在求解浮点约束时与当前最优 SMT 求解器既有竞争力又互补，且覆盖率引导相比朴素模糊测试在浮点域带来显著收益；以 portfolio 方式使用可补充传统 SMT 求解器。
We investigate the use of coverage-guided fuzzing as a means of proving satisfiability of SMT formulas over finite variable domains, with specific application to floating-point constraints. We show how an SMT formula can be encoded as a program containing a location that is reachable if and only if the program’s input corresponds to a satisfying assignment to the formula. A coverage-guided fuzzer can then be used to search for an input that reaches the location, yielding a satisfying assignment. We have implemented this idea in a tool, Just Fuzz-it Solver (JFS), and we present a large experimental evaluation showing that JFS is both competitive with and complementary to state-of-the-art SMT solvers with respect to solving floating-point constraints, and that the coverage-guided approach of JFS provides significant benefit over naive fuzzing in the floating-point domain. Applied in a portfolio manner, the JFS approach thus has the potential to complement traditional SMT solvers for program analysis tasks that involve reasoning about floating-point constraints.
DOI 原文 ·
@inproceedings{paperbot5102,
title = {Just fuzz it: solving floating-point constraints using coverage-guided fuzzing},
author = {Daniel Liew and Cristian Cadar and Alastair F. Donaldson and J. Ryan Stinnett},
booktitle = {FSE},
year = {2019},
doi = {10.1145/3338906.3338921}
}