On the unusual effectiveness of type-aware operator mutations for testing SMT solvers
Read the paper · doi:10.1145/3428261 · arXiv:2004.08799v4
What this paper does with SQLancer
SQLancer appears once, in a list of domains where testing has been applied, cited alongside work on SMT solvers and OS kernels. Nothing in the paper connects to it beyond that.
Type-aware operator mutation tests SMT solvers by mutating operators of conforming types within seed formulas to produce well-typed mutants used as test cases. Realised in OpFuzz and applied to Z3 and CVC4, it proved unusually effective: over a year the authors reported 1,092 bugs, 819 confirmed and 685 fixed, spanning soundness bugs, invalid model bugs and crashes. A follow-up study found the bugs were high quality, often affecting core components.
How it was classified
uses infrastructure — no
SQLancer is cited, not used; nothing in the mentions describes reusing its code.
extends technique — no
No technique is extended; the citation is background.
compares with — no
No empirical comparison against SQLancer is reported in the mentions.
describes as state of the art — no
The citation does not characterise SQLancer as the state of the art.
Every place it refers to SQLancer (1)
1 sentence, each stored verbatim from the extracted text with where it was found and how. “Citation marker” means the sentence names no tool at all and was reached through a reference number that resolved to a SQLancer publication.
| Id | Sentence | Found by | Where |
|---|---|---|---|
| M1 | 2008; Rigger and Su 2020; Seltenreich 2020], and testing OS kernel [Corina et al . |
author year citation |
5.3 Assorted Bug Samples page 22 |