Metadata only
Date
2022-10Type
- Conference Paper
Abstract
We 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 SMT solvers unexpectedly return 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 31 incompleteness bugs. Out of these, 26 have been confirmed as unique bugs and 19 are already fixed by the developers. Our diverse bug findings uncovered functional, regression, and performance bugs—several triggered discussions among the developers sharing their in-depth analysis. Show more
Publication status
publishedExternal links
Book title
ASE '22: Proceedings of the 37th IEEE/ACM International Conference on Automated Software EngineeringPages / Article No.
Publisher
Association for Computing MachineryEvent
Organisational unit
09628 - Su, Zhendong / Su, Zhendong
More
Show all metadata