一句话：提出以边界条件引导的 LTL 求解器模糊测试方法 SpecBCFuzz，发现大量真实缺陷。
LTL 求解器判定线性时序逻辑公式可满足性，是验证和测试关键软件的重要工具，其实现缺陷影响重大。本文提出 SpecBCFuzz，一种边界条件（BC）引导的 LTL 求解器模糊测试方法；BC 是可满足性取决于稀有迹的极端情形。该方法采用基于搜索的算法生成公式并优先关注 BC，结合语法与语义相似度在带 BC 的种子公式附近探索。作者在 NuSMV、Black、Aalta、PLTL 四个求解器的 21 个配置上评估，生成 368,716 个触发缺陷公式，在 18 个配置中发现缺陷，包括 Aalta/PLTL 的可靠性问题、NuSMV/Black/Aalta 的崩溃、NuSMV/Aalta 的不稳定行为及 Black/Aalta/PLTL 的性能退化；NuSMV BDD 各版本未发现缺陷。
LTL solvers check the satisfiability of Linear-time Temporal Logic (LTL) formulas and are widely used for verifying and testing critical software systems. Thus, potential bugs in the solvers' implementations can have a significant impact. We present SpecBCFuzz, a fuzzing method for finding bugs in LTL solvers, that is guided by boundary conditions (BCs), corner cases whose (un)satisfiability depends on rare traces. SpecBCFuzz implements a search-based algorithm that fuzzes LTL formulas giving relevance to BCs. It integrates syntactic and semantic similarity metrics to explore the vicinity of the seeded formulas with BCs. We evaluate SpecBCFuzz on 21 different configurations (including the latest and past releases) of four mature and state-of-the-art LTL solvers (NuSMV, Black, Aalta, and PLTL) that implement a diverse set of satisfiability algorithms. SpecBCFuzz produces 368,716 bug-triggering formulas, detecting bugs in 18 out of the 21 solvers' configurations we study. Overall, SpecBCFuzz reveals: soundness issues (wrong answers given by a solver) in Aalta and PLTL; crashes, e.g., segmentation faults, in NuSMV, Black and Aalta; flaky behaviors (different responses across re-runs of the solver on the same formula) in NuSMV and Aalta; performance bugs (large time performance degradation between successive versions of the solver on the same formula) in Black, Aalta and PLTL; and no bug in NuSMV BDD (all versions), suggesting that the latter is currently the most robust solver.
@inproceedings{paperbot11362,
title = {SpecBCFuzz: Fuzzing LTL Solvers with Boundary Conditions},
author = {Luiz Carvalho and Renzo Degiovanni and Maxime Cordy and Nazareno Aguirre and Yves Le Traon and Mike Papadakis},
booktitle = {ICSE},
year = {2024},
doi = {10.1145/3597503.3639087}
}