Yin-Yang – A tool for stress-testing SMT solvers
testsmt.github.io
Yin-Yang – A tool for stress-testing SMT solvers
1–10 of 15 posts
Re: Yin-Yang – A tool for stress-testing SMT solvers
#2Project website: https://testsmt.github.io/
Re: Yin-Yang – A tool for stress-testing SMT solvers
#3It's verification-verifiers all the way down.
Re: Yin-Yang – A tool for stress-testing SMT solvers
#4Any ideas why Z3 has so many more issues than CVC4?
Maybe because CVC4 has better practices around fuzzing? https://github.com/CVC4/CVC4/wiki/Fuzzing-CVC4 Not sure.
I am also looking for a recommendation for a survey comparing different SMT solvers, including e.g. https://github.com/SRI-CSL/yices2 and https://github.com/dreal/dreal4
Re: Yin-Yang – A tool for stress-testing SMT solvers
#5This video illustrates the principle well: https://www.youtube.com/watch?v=hEWpbO5yXPw
Re: Yin-Yang – A tool for stress-testing SMT solvers
#6Any ideas why Z3 has so many more issues than CVC4? Maybe because CVC4 has better practices around fuzzing? https://github.com/CVC4/CVC4/wiki/Fuzzing-CVC4 Not sure. I am also looking for a recommendation for a survey comparing different SMT solvers, including e.g. https://github.com/SRI-CSL/yices2 and https://github.com/dreal/dreal4
Good question, gugagore!
We have treated Z3 and CVC4 exactly equal, i.e. every formula on which Z3 was tested, CVC4 got also tested. It is thus striking that we found almost twice as many bugs in Z3 as compared to CVC4. The solvers have different development models. Whereas Z3 relies on a single main developer and a couple of assisting developers, CVC4 is more of a community effort. CVC4 requires code reviews, Z3 usually not. On the other hand, issues in Z3 get usually fixed faster and Z3 has the larger codebase (Z3: ~400k LoC vs CVC4: ~200k LoC). The fuzzing practices of CVC4 did not play a role, though. As soon as they were in place (since August 2020), we applied their rules to both solvers. Our earlier work "Validating SMT Solvers via Semantic Fusion" published at PLDI 2020 (bug hunting from July 2019 - November 2019) showed the same trend. To the best of our knowledge, all SMT solver bug hunting campaigns prior to ours, found no bugs in CVC4 at all. CVC4 simply seems to be harder to crack.
Re: Yin-Yang – A tool for stress-testing SMT solvers
#7"Come on Richard. Yin and Yang? Pretty sure it's Ying and Yang." - Ron LaFlamme
Re: Yin-Yang – A tool for stress-testing SMT solvers
#8Any ideas why Z3 has so many more issues than CVC4? Maybe because CVC4 has better practices around fuzzing? https://github.com/CVC4/CVC4/wiki/Fuzzing-CVC4 Not sure. I am also looking for a recommendation for a survey comparing different SMT solvers, including e.g. https://github.com/SRI-CSL/yices2 and https://github.com/dreal/dreal4
Good question, gugagore! We have treated Z3 and CVC4 exactly equal, i.e. every formula on which Z3 was tested, CVC4 got also tested. It is thus striking that we found almost twice as many bugs in Z3 as compared to CVC4. The solvers have different development models. Whereas Z3 relies on a single main developer and a couple of assisting developers, CVC4 is more of a community effort. CVC4 requires code reviews, Z3 usu…
To add a quick follow-up to dwinterer's nice reply, note please Z3's current support for nonlinear arithmetic and string logics is more advanced than CVC4's, where many of the detected bugs in Z3 occurred.
Re: Yin-Yang – A tool for stress-testing SMT solvers
#9Earlier quoted context omitted.
Good question, gugagore! We have treated Z3 and CVC4 exactly equal, i.e. every formula on which Z3 was tested, CVC4 got also tested. It is thus striking that we found almost twice as many bugs in Z3 as compared to CVC4. The solvers have different development models. Whereas Z3 relies on a single main developer and a couple of assisting developers, CVC4 is more of a community effort. CVC4 requires code reviews, Z3 usu…
To add a quick follow-up to dwinterer's nice reply, note please Z3's current support for nonlinear arithmetic and string logics is more advanced than CVC4's, where many of the detected bugs in Z3 occurred.
Figure 8 in the OOPSLA paper (https://arxiv.org/pdf/2004.08799.pdf) provides a breakdown of the bugs found in different logics for Z3 and CVC4.
Re: Yin-Yang – A tool for stress-testing SMT solvers
#10This video illustrates the principle well: https://www.youtube.com/watch?v=hEWpbO5yXPw
Good video!
It could have been improved by digging into why the code of Z3 and CVC4 had those bugs.
It is surprising to me that they could be wrong on such simple statements (and such a simple fuzzing procedure). I expected the faulty statements to be gigantic edge-case monstrosities, but they are just a few lines of boolean logic.