Show simple item record

dc.contributor.author
Winterer, Dominik
dc.contributor.author
Zhang, Chengyu
dc.contributor.author
Su, Zhendong
dc.date.accessioned
2022-12-06T09:58:03Z
dc.date.available
2020-12-17T19:37:05Z
dc.date.available
2020-12-18T13:50:04Z
dc.date.available
2021-01-11T09:40:09Z
dc.date.available
2022-12-06T09:58:03Z
dc.date.issued
2020-11
dc.identifier.issn
2475-1421
dc.identifier.other
10.1145/3428261
en_US
dc.identifier.uri
http://hdl.handle.net/20.500.11850/456968
dc.identifier.doi
10.3929/ethz-b-000456968
dc.description.abstract
We propose type-aware operator mutation, a simple, but unusually effective approach for testing SMT solvers. The key idea is to mutate operators of conforming types within the seed formulas to generate well-typed mutant formulas. These mutant formulas are then used as the test cases for SMT solvers. We realized type-aware operator mutation within the OpFuzz tool and used it to stress-test Z3 and CVC4, two state-of-the-art SMT solvers. Type-aware operator mutations are unusually effective: During one year of extensive testing with OpFuzz, we reported 1092 bugs on Z3’s and CVC4’s respective GitHub issue trackers, out of which 819 unique bugs were confirmed and 685 of the confirmed bugs were fixed by the developers. The detected bugs are highly diverse — we found bugs of many different types (soundness bugs, invalid model bugs, crashes, etc.), logics and solver configurations. We have further conducted an in-depth study of the bugs found by OpFuzz. The study results show that the bugs found by OpFuzz are of high quality. Many of them affect core components of the SMT solvers’ codebases, and some required major changes for the developers to fix. Among the 819 confirmed bugs found by OpFuzz,184 were soundness bugs, the most critical bugs in SMT solvers,and 489 were in the default modes of the solvers. Notably, OpFuzz found 27 critical soundness bugs in CVC4, which has proved to be a very stable SMT solver.
en_US
dc.format
application/pdf
en_US
dc.language.iso
en
en_US
dc.publisher
Association for Computing Machinery
en_US
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
dc.subject
SMT solvers
en_US
dc.subject
Fuzz testing
en_US
dc.subject
Type-aware operator mutation
en_US
dc.title
On the unusual effectiveness of type-aware operator mutations for testing SMT solvers
en_US
dc.type
Conference Paper
dc.rights.license
Creative Commons Attribution 4.0 International
dc.date.published
2020-11-13
ethz.journal.title
Proceedings of the ACM on Programming Languages
ethz.journal.volume
4
en_US
ethz.journal.issue
OOPSLA
en_US
ethz.journal.abbreviated
Proc. ACM Program. Lang.
ethz.pages.start
193
en_US
ethz.size
25 p.
en_US
ethz.version.deposit
publishedVersion
en_US
ethz.event
Object-oriented Programming, Systems, Languages, and Applications Conference (OOPSLA 2020)
en_US
ethz.event.location
Online
en_US
ethz.event.date
November 15-21, 2020
en_US
ethz.identifier.wos
ethz.identifier.scopus
ethz.publication.place
New York, NY
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::09628 - Su, Zhendong / Su, Zhendong
en_US
ethz.leitzahl.certified
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::09628 - Su, Zhendong / Su, Zhendong
en_US
ethz.date.deposited
2020-12-17T19:37:14Z
ethz.source
FORM
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2020-12-18T13:50:13Z
ethz.rosetta.lastUpdated
2023-02-07T08:31:38Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=On%20the%20unusual%20effectiveness%20of%20type-aware%20operator%20mutations%20for%20testing%20SMT%20solvers&rft.jtitle=Proceedings%20of%20the%20ACM%20on%20Programming%20Languages&rft.date=2020-11&rft.volume=4&rft.issue=OOPSLA&rft.spage=193&rft.issn=2475-1421&rft.au=Winterer,%20Dominik&Zhang,%20Chengyu&Su,%20Zhendong&rft.genre=proceeding&rft_id=info:doi/10.1145/3428261&
 Search print copy at ETH Library

Files in this item

Thumbnail

Publication type

Show simple item record