menu

Validating SMT Solvers via Semantic Fusion

Winterer, Dominik and Zhang, Chengyu and Su, Zhendong

PDF

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.


@inproceedings{winterer-pldi20,
  address = {New York, NY, USA},
  author = {Winterer, Dominik and Zhang, Chengyu and Su, Zhendong},
  booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation},
  date-added = {2020-11-16 00:08:54 -0800},
  date-modified = {2020-11-16 00:09:03 -0800},
  doi = {10.1145/3385412.3385985},
  isbn = {9781450376136},
  keywords = {Semantic fusion, Fuzz testing, SMT solvers},
  location = {London, UK},
  numpages = {13},
  pages = {718--730},
  publisher = {Association for Computing Machinery},
  series = {PLDI 2020},
  title = {Validating SMT Solvers via Semantic Fusion},
  url = {https://doi.org/10.1145/3385412.3385985},
  year = {2020},
  bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAccGFwZXJzL3dpbnRlcmVyLXBsZGkyMC1hLnBkZk8RAXwAAAAAAXwAAgAADE1hY2ludG9zaCBIRAAAAAAAAAAAAAAAAAAAAAAAAABCRAAB/////xV3aW50ZXJlci1wbGRpMjAtYS5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAD/////AAAAAAAAAAAAAAAAAAEAAwAACiBjdQAAAAAAAAAAAAAAAAAGcGFwZXJzAAIAOy86VXNlcnM6Z2FtYmxpbjI6c3JjOmJ1aWxkLWJpYjpwYXBlcnM6d2ludGVyZXItcGxkaTIwLWEucGRmAAAOACwAFQB3AGkAbgB0AGUAcgBlAHIALQBwAGwAZABpADIAMAAtAGEALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASADlVc2Vycy9nYW1ibGluMi9zcmMvYnVpbGQtYmliL3BhcGVycy93aW50ZXJlci1wbGRpMjAtYS5wZGYAABMAAS8AABUAAgAP//8AAAAIAA0AGgAkAEMAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAABww==},
  bdsk-url-1 = {https://doi.org/10.1145/3385412.3385985}
}
Top