Show simple item record

dc.contributor.author
Winterer, Dominik
dc.contributor.author
Zhang, Chengyu
dc.contributor.author
Su, Zhendong
dc.contributor.editor
Donaldson, Alastair F.
dc.contributor.editor
Torlak, Emina
dc.date.accessioned
2020-08-04T09:25:39Z
dc.date.available
2020-07-01T02:45:55Z
dc.date.available
2020-08-04T09:25:39Z
dc.date.issued
2020-06
dc.identifier.isbn
978-1-4503-7613-6
en_US
dc.identifier.other
10.1145/3385412.3385985
en_US
dc.identifier.uri
http://hdl.handle.net/20.500.11850/423885
dc.description.abstract
We introduce Semantic Fusion, a general, effective methodology for validating Satisfiability Modulo Theory (SMT) solvers. Our key idea is to fuse two existing equisatisfiable (i.e., both satisfiable or unsatisfiable) formulas into a new formula that combines the structures of its ancestors in a novel manner and preserves the satisfiability by construction. This fused formula is then used for validating SMT solvers. We realized Semantic Fusion as YinYang, a practical SMT solver testing tool. During four months of extensive testing, YinYang has found 45 confirmed, unique bugs in the default arithmetic and string solvers of Z3 and CVC4, the two state-of-the-art SMT solvers. Among these, 41 have already been fixed by the developers. The majority (29/45) of these bugs expose critical soundness issues. Our bug reports and testing effort have been well-appreciated by SMT solver developers. © 2020 ACM.
en_US
dc.language.iso
en
en_US
dc.publisher
Association for Computing Machinery
en_US
dc.subject
Fuzz testing
en_US
dc.subject
Semantic fusion
en_US
dc.subject
SMT solvers
en_US
dc.title
Validating SMT solvers via semantic fusion
en_US
dc.type
Conference Paper
ethz.book.title
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
en_US
ethz.pages.start
718
en_US
ethz.pages.end
730
en_US
ethz.event
41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020) (virtual)
en_US
ethz.event.location
London, United Kingdom
ethz.event.date
June 15-20, 2020
ethz.notes
Due to the Corona virus (COVID-19) the conference was conducted virtually.
en_US
ethz.identifier.wos
ethz.identifier.scopus
ethz.publication.place
New York, NY
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
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
ethz.date.deposited
2020-07-01T02:46:08Z
ethz.source
SCOPUS
ethz.eth
yes
en_US
ethz.availability
Metadata only
en_US
ethz.rosetta.installDate
2020-08-04T09:25:57Z
ethz.rosetta.lastUpdated
2024-02-02T11:31:35Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Validating%20SMT%20solvers%20via%20semantic%20fusion&rft.date=2020-06&rft.spage=718&rft.epage=730&rft.au=Winterer,%20Dominik&Zhang,%20Chengyu&Su,%20Zhendong&rft.isbn=978-1-4503-7613-6&rft.genre=proceeding&rft_id=info:doi/10.1145/3385412.3385985&rft.btitle=Proceedings%20of%20the%2041st%20ACM%20SIGPLAN%20Conference%20on%20Programming%20Language%20Design%20and%20Implementation
 Search print copy at ETH Library

Files in this item

FilesSizeFormatOpen in viewer

There are no files associated with this item.

Publication type

Show simple item record