Skeletal approximation enumeration for SMT solver testing

Peisen Yao, Heqing Huang, Wensheng Tang, Qingkai Shi, Rongxin Wu, Charles Zhang. 2021. ESEC/SIGSOFT FSE.

Read the paper · doi:10.1145/3468264.3468540

What this paper does with SQLancer

Databases appear in a single sentence listing the application domains where the underlying technique has been used, alongside bioinformatics, compilers, debuggers and machine learning systems. The mention is reachable only through the citation marker and establishes breadth of applicability rather than any relationship to SQLancer. This work tests SMT solvers by enumerating skeletal approximations of a formula -- systematically weakened versions whose satisfiability stands in a known relation to the original -- giving an oracle without a reference solver. Written by claude-opus-5 from the 1 place this paper refers to SQLancer. The quotations below are the paper's own words, stored verbatim when the text was extracted.

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.

SQLancer publications it cites (1)

Bibliography entries that resolved to a SQLancer publication, or to a paper by one of the project's authors. A sentence citing one of these numbers is a reference to SQLancer even when it never writes the name.

#	Entry	Matched as
47	Manuel Rigger and Zhendong Su. 2020. Finding Bugs in Database Systems via Query Partitioning. Proc. ACM Program. Lang. 4, OOPSLA, Article 211 (Nov. 2020), 30 pages. https://doi.org/10.1145/3428279	sqlancer publication · TLP

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	in many application domains such as bioinformatics [ 26], web services [ 24], compilers [ 36,51], debuggers [ 53], databases [ 47], machine learning-based systems [ 31,38], model counters [ 55], and SMT solvers [60].	citation marker background	6 DISCUSSION page 11

This page is rendered from _data/papers/paper_doi_10_1145_3468264_3468540.json, extracted from supplied pdf. 13 pages, 63 references parsed.