Generative type-aware mutation for testing SMT solvers
Read the paper · doi:10.1145/3485529
What this paper does with SQLancer
PQS appears in the evaluation setup's survey of generative fuzzing approaches, cited in the ACM author-year style so SQLancer is not named directly. The paper places it alongside Csmith and YarpGen as recent generative fuzzers, and distinguishes it as the metamorphic one of the group -- checking a relation between two runs rather than comparing against an independent reference.
TypeFuzz tests SMT solvers with generative type-aware mutation, splicing well-typed expressions from one formula into another so the result stays well-typed and reaches deeper into the solver. The technique is for constraint solvers rather than databases, and the paper surveys generative fuzzing across domains.
How it was classified
uses infrastructure — no
SQLancer is cited as related work; no reuse of its code, generator or workload is described.
extends technique — no
No SQLancer technique is extended; the citation is background.
compares with — no
No empirical comparison against SQLancer or one of its oracles is reported.
describes as state of the art — no
The text does not describe SQLancer as the state of the art.
Every place it refers to SQLancer (2)
2 sentences, 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 | Anotherrecentgenerativefuzzingapproachispivotquerysynthesis(PQS)[ Riggerand Su2020]. |
technique |
4.1 EvaluationSetup page 17 |
| M2 | UnlikeCsmithandYarpGen, PQS’s is a metamorphic testing approach. |
technique |
4.1 EvaluationSetup page 17 |