Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations

Jongwook Kim, Sunbeom So, Hakjoo Oh

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present Diver, a novel technique for effectively finding critical bugs in SMT solvers. Ensuring the correctness of SMT solvers is becoming increasingly important as many applications use solvers as a foundational basis. In response, several approaches for testing SMT solvers, which are classified into differential testing and oracle-guided approaches, have been proposed until recently. However, they are still unsatisfactory in that (1) differential testing approaches cannot validate unique yet important features of solvers, and (2) oracle-guided approaches cannot generate diverse tests due to their reliance on limited mutation rules. Diver aims to complement these shortcomings, particularly focusing on finding bugs that are missed by existing approaches. To this end, we present a new testing technique that performs oracle-guided yet unrestricted random mutations. We have used Diver to validate the most recent versions of three popular SMT solvers: CVC5, Z3 and dReal. In total, Diver found 25 new bugs, of which 21 are critical and directly affect the reliability of the solvers. We also empirically prove DIVER's own strength by showing that existing tools are unlikely to find the bugs discovered by Diver.

Original languageEnglish
Title of host publicationProceedings - 2023 IEEE/ACM 45th International Conference on Software Engineering, ICSE 2023
PublisherIEEE Computer Society
Pages2224-2236
Number of pages13
ISBN (Electronic)9781665457019
DOIs
Publication statusPublished - 2023
Event45th IEEE/ACM International Conference on Software Engineering, ICSE 2023 - Melbourne, Australia
Duration: 2023 May 152023 May 16

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257

Conference

Conference45th IEEE/ACM International Conference on Software Engineering, ICSE 2023
Country/TerritoryAustralia
CityMelbourne
Period23/5/1523/5/16

Bibliographical note

Publisher Copyright:
© 2023 IEEE.

Keywords

  • SMT solver
  • fuzzing
  • software testing

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations'. Together they form a unique fingerprint.

Cite this