CoChat
Sign Up
Cited by 53Software Testing and Debugging TechniquesFormal Methods in VerificationLogic, programming, and type systems

Detecting critical bugs in SMT solvers using blackbox mutational fuzzing

Open access
Mansur, Muhammad Numair, Christakis, Maria, Wüstholz, Valentin, Zhang, Fuyuan·2020·Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
DOI 10.1145/3368089.3409763
Open this paper in CoChat — free accountOpen PDF

Abstract

Formal methods use SMT solvers extensively for deciding formula satisfiability, for instance, in software verification, systematic test generation, and program synthesis. However, due to their complex implementations, solvers may contain critical bugs that lead to unsound results. Given the wide applicability of solvers in software reliability, relying on such unsound results may have detrimental consequences. In this paper, we present STORM, a novel blackbox mutational fuzzing technique for detecting critical bugs in SMT solvers. We run our fuzzer on seven mature solvers and find 29 previously unknown critical bugs. STORM is already being used in testing new features of popular solvers before deployment.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1145/3368089.3409763

Cites

2 of 2 references verified0 citation errors · 0 not checkable

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Correctness in Dafny relies on the soundness of the SMT solver (e.g., Z3), a massive software system with a known history of bugs.

    “Correctness relies on the soundness of the SMT solver (e.g., Z3), a massive software system with a known history of bugs (Mansur et al., 2020;Winterer et al., 2020).”

    From AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms (2026) · cites this paper as Mansur et al., 2020

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

Flagged first, then by citations

Research works printed but not linked: 35

  1. Cyrille Artho, Armin Biere, and Martina Seidl. 2013. Model-Based Testing for Verification Back-Ends. In TAP (LNCS, Vol. 7942). Springer, 39-55.
  2. Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rus- tan M. Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO (LNCS, Vol. 4111). Springer, 364-387.
  3. Earl T. Barr, Mark Harman, Phil McMinn, Muzammil Shahbaz, and Shin Yoo. 2015. The Oracle Problem in Software Testing: A Survey. TSE 41 (2015), 507-525. Issue 5.
  4. Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In CAV (LNCS, Vol. 6806). Springer, 171-177.
  5. Clark W. Barrett and Cesare Tinelli. 2018. Satisfiability Modulo Theories. In Handbook of Model Checking. Springer, 305-343.
  6. Murphy Berzish, Vijay Ganesh, and Yunhui Zheng. 2017. Z3str3: A String Solver with Theory-Aware Heuristics. In FMCAD. IEEE Computer Society, 55-59.
  7. Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, and Vijay Ganesh. 2018. StringFuzz: A Fuzzer for String Solvers. In CAV (LNCS, Vol. 10982). Springer, 45-51.
  8. Robert Brummayer and Armin Biere. 2009. Fuzzing and Delta-Debugging SMT Solvers. In SMT. ACM, 1-5.
  9. Robert Brummayer, Florian Lonsing, and Armin Biere. 2010. Automated Testing and Debugging of SAT and QBF Solvers. In SAT (LNCS, Vol. 6175). Springer, 44-57.
  10. Alexandra Bugariu and Peter Müller. 2020. Automatically Testing String Solvers. In ICSE. To appear.
  11. Alexandra Bugariu, Valentin Wüstholz, Maria Christakis, and Peter Müller. 2018. Automatically Testing Implementations of Numerical Abstract Domains. In ASE. ACM, 768-778.
  12. Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI. USENIX, 209-224.
  13. Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. 2012. SMTInterpol: An Interpolating SMT Solver. In SPIN (LNCS, Vol. 7385). Springer, 248-254.
  14. Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. 2013. The MathSAT5 SMT Solver. In TACAS (LNCS, Vol. 7795). Springer, 93-107.
  15. Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In POPL. ACM, 238-252.
  16. Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John Regehr, Boris Yakobowski, and Xuejun Yang. 2012. Testing Static Analyzers with Randomly Generated Programs. In NFM (LNCS, Vol. 7226). Springer, 120-125.
  17. Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In TACAS (LNCS, Vol. 4963). Springer, 337-340.
  18. Leonardo de Moura and Dejan Jovanovic. 2013. A Model-Constructing Satisfia- bility Calculus. In VMCAI (LNCS, Vol. 7737). Springer, 1-12.
  19. Bruno Dutertre. 2014. Yices 2.2. In CAV (LNCS, Vol. 8559). Springer, 737-744.
  20. Jonathan Ford and Natarajan Shankar. 2002. Formal Verification of a Combination Decision Procedure. In CADE (LNCS, Vol. 2392). Springer, 347-362.
  21. Vijay Ganesh. 2007. Decision Procedures for Bit-Vectors, Arrays and Integers. Ph.D. Dissertation. Stanford University, USA.
  22. Vijay Ganesh and David L. Dill. 2007. A Decision Procedure for Bit-Vectors and Arrays. In CAV (LNCS, Vol. 4590). Springer, 519-531.
  23. Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008. Automated Whitebox Fuzz Testing. In NDSS. The Internet Society, 151-166.
  24. Dejan Jovanovic, Clark Barrett, and Leonardo de Moura. 2013. The Design and Implementation of the Model-Constructing Satisfiability Calculus. In FMCAD. IEEE Computer Society, 173-180.
  25. Timotej Kapus and Cristian Cadar. 2017. Automatic Testing of Symbolic Execution Engines via Program Generation and Differential Testing. In ASE. IEEE Computer Society, 590-600.
  26. Christian Klinger, Maria Christakis, and Valentin Wüstholz. 2019. Differentially Testing Soundness and Precision of Program Analyzers. In ISSTA. ACM, 239-250.
  27. Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. 2015. Provably Correct Peephole Optimizations with Alive. In PLDI. ACM, 22-32.
  28. Filip Maric. 2010. Formal Verification of a Modern SAT Solver by Shallow Em- bedding into Isabelle/HOL. TCS 411 (2010), 4333-4356. Issue 50.
  29. Lorenzo Martignoni, Stephen McCamant, Pongsin Poosankam, Dawn Song, and Petros Maniatis. 2012. Path-Exploration Lifting: Hi-Fi Tests for Lo-Fi Emulators. In ASPLOS. ACM, 337-348.
  30. William M. McKeeman. 1998. Differential Testing for Software. Digital Technical Journal 10 (1998), 100-107. Issue 1.
  31. Aina Niemetz, Mathias Preiner, Clifford Wolf, and Armin Biere. 2018. Btor2, BtorMC and Boolector 3.0. In CAV (LNCS, Vol. 10981). Springer, 587-595.
  32. Janet Siegmund, Norbert Siegmund, and Sven Apel. 2015. Views on Internal and External Validity in Empirical Software Engineering. In ICSE. IEEE Computer Society, 9-19.
  33. Jubi Taneja, Zhengyang Liu, and John Regehr. 2020. Testing Static Analyses for Precision and Soundness. In CGO. ACM, 81-93.
  34. Andreas Zeller. 2009. Why Programs Fail, Second Edition: A Guide to Systematic Debugging. Morgan Kaufmann.
  35. Chengyu Zhang, Ting Su, Yichen Yan, Fuyuan Zhang, Geguang Pu, and Zhendong Su. 2019. Finding and Understanding Bugs in Software Model Checkers. In ESEC/FSE. ACM, 763-773.

Cited by

Sorted by citations

Authors
Mansur, M. N., Christakis, M., Wüstholz, V., & Zhang, F.
Affiliations
  • Max Planck Institute for Software Systems (DE)
  • ConsenSys (United States) (US)
ORCID
Venue
Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
Publisher
ACM
Published
2020-11-08
Pages
701-712
DOI
10.1145/3368089.3409763
OpenAlex
W3104402823
Cited by
53
References
2
Citations by year
2026: 8 · 2025: 10 · 2024: 5 · 2023: 9 · 2022: 10 · 2021: 8 · 2020: 3
FWCI
4.90
Type
conference paper
Language
en
Open access
Licence
Locations
  • ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) (publishedVersion, cc-by)
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Funders
German Research Foundation (DFG) (389792660 (TRR 248))
Topics
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
Keywords
SMT solvers, bug detection, storms, satisfiability solving, software verification, program synthesis

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review