
Registered user since Sun 26 Aug 2018
Contributions
View general profile
Registered user since Sun 26 Aug 2018
Contributions
Research Papers
Thu 13 Oct 2022 16:50 - 17:10 at Banquet B - Technical Session 32 - Formal Methods and Models II Chair(s): Khouloud GaaloulWe propose Janus, an approach for finding incompleteness bugs in SMT solvers. The key insight is to mutate SMT formulas with local weakening and strengthening rules that preserve the satisfiability of the seed formula. The generated mutants are used to test SMT solvers for incompleteness bugs, i.e., inputs on which the SMT solver unexpectedly returns unknown. We realized Janus on top of the SMT solver fuzzing framework YinYang. From June to August 2021, we stress-tested the two state-of-the-art SMT solvers Z3 and CVC5 with Janus and totally reported 32 incompleteness bugs. Out of these, 24 have been confirmed as unique bugs and 8 are already fixed by the developers. Our diverse bug findings uncovered functional, regression, and performance bugs—several surprising enough to trigger discussions among the developers sharing their in-depth analysis.