The DOI matches its Crossref record; 57 of the 57 references it cites were found in a registry or an index; none of the 14 sources its claims cite is checked for support yet.
Syntax-guided synthesis
Open accessAbstract
The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations. Our goal is to identify the core computational problem common to these proposals in a logical framework. The input to the syntax-guided synthesis problem (SyGuS) consists of a background theory, a semantic correctness specification for the desired program given by a logical formula, and a syntactic set of candidate implementations given by a grammar. The computational problem then is to find an implementation from the set of candidate expressions so that it satisfies the specification in the given theory. We describe three different instantiations of the counter-example-guided-inductive-synthesis (CEGIS) strategy for solving the synthesis problem, report on prototype implementations, and present experimental results on an initial set of benchmarks.
Overview
AI snapshot
Written from the paper’s full text.
TL;DR
This paper formalizes syntax-guided synthesis (SyGuS): given a background theory, a logical correctness specification, and a grammar of candidate expressions, find an expression satisfying the specification. It describes three CEGIS-based prototype solvers—enumerative, symbolic/constraint-based, and stochastic—and reports an initial benchmark comparison.
Key findings
- The SyGuS problem is defined as: given theory \(T\), typed function symbol \(f\), formula \(\phi\), and candidate set \(L\), find \(e \in L\) such that \(\phi[f/e]\) is valid modulo \(T\); the paper also proposes a SYNTH-LIB input format based on SMT-LIB2.
- Three CEGIS instantiations are implemented: enumerative learning, constraint-based/symbolic learning, and stochastic search; in the illustrative max example, the enumerative solver found the correct expression after only four SMT calls although about 200 expressions were enumerated and only about 80 stored.
- On 57 Hacker’s Delight benchmarks derived from 20 bit-manipulation problems, the enumerative solver dominated, followed by stochastic, while symbolic was slowest and failed to terminate on 29 of 57.
- For integer benchmarks, no solver synthesized array-search for \(n > 4\); enumerative was fastest except max3, where stochastic was faster. For parity Boolean/bit-vector benchmarks, enumerative was always faster and symbolic failed every instance; Morton benchmarks were not completed by any synthesizer.
Methods
- The paper gives a logical problem formulation with a background theory, a universally quantified first-order correctness specification, and a context-free grammar defining the candidate expression set; it also discusses encodings for multiple functions and let-expressions.
- The solving architecture is counterexample-guided inductive synthesis (CEGIS): a learning algorithm proposes a candidate from accumulated examples, and a verification oracle—implemented with an SMT solver—checks validity and returns counterexamples until a correct candidate is found or learning fails.
- The three learning strategies are: enumerative dynamic-programming search over increasing expression size with example-based pruning; symbolic component-based synthesis of loop-free programs with typing constraints and incremental SMT constraints; and stochastic Metropolis-Hastings search over parse trees with score \(\exp(-\beta C(e))\), default \(\beta=0.5\), and concurrent searches over expression sizes.
Limitations
- Stated: the current benchmark set is limited to synthesis of loop-free functions with no optimality criterion; the number of benchmarks and maturity of solvers are too limited to draw broad conclusions; prototypes were not engineered for high performance, so exact solution times are not necessarily representative.
- Stated: the symbolic solver uses a direct encoding and off-the-shelf Z3 rather than a synthesis-tuned solver, and the comparison with Sketch is “not an entirely fair comparison.”
- Evident from the text: several benchmarks timed out or could not be solved by any prototype, and the paper reports that problem encoding into grammar significantly affects performance, so the relative merits observed are preliminary.
Model-written summary. Check it against the paper before relying on it.
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
0 of 14 cited sources checked · 0 supported · 0 flagged
In the paper
“This set includes 57 different benchmarks derived from 20 different bit-manipulation problems from the book Hacker's Delight [27].”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
What the sources say
- Not matchedcites [27]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passes- Not matched
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Moreover, we observe that the enumerative technique was better than the stochastic search for all but two benchmarks,”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesA result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“We can see in the data that all solvers were affected by the encoding of the problem for at least some benchmark;”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Moreover, the enumerative solver was able to solve more hd problems than even the more optimized symbolic solver.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“This benchmark proved to be quite complex, as no solver was able to synthesize this function for n > 4.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The exception was max3 where the stochastic solver was faster.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedSingle caseTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“although in some cases, the pruning strategies used by the solvers were able to ameliorate the impact of the larger search space.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesThe paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“On the other hand, the more optimized symbolic solver did have a significant advantage in the array-search benchmarks which the enumerative solver could only solve up to size 4.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Although adding support for multiple functions does not fundamentally increase the expressiveness of the notation, it does offer significant convenience in encoding real-world synthesis problems.”
§ Syntax-Guided Synthesis > Synthesis of Multiple Functions:
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“In principle, adding support for problems with more than one unknown function is merely a matter of syntactic sugar.”
§ Syntax-Guided Synthesis > Synthesis of Multiple Functions:
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passes
- Probably not a substantial claim. 40
- It may state two separate claims as one. 31
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Thus, the mutation e = ITE(0 ≤ y, y, x) is considered with probability 1/288.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“As with other benchmarks, the enumerative solver was always faster, whereas the symbolic solver failed on every instance.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:correlational· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Aimed at formulating the core computational problem common to many recent tools for program synthesis in a canonical and logical manner, we have formalized the problem of syntax-guided synthesis.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“In the example we have described, the correct expression was examined after only four calls to the SMT solver, although about 200 expressions were enumerated by the algorithm.”
§ Syntax-Guided Synthesis > D. Enumerative Learning
Strength:plain· not yet calibratedSingle caseTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Thus, the probability of choosing e = ITE(x ≤ 0, y, x) as the initial candidate is 1/768.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“For the Hacker's Delight benchmarks (hd) we see that the enumerative solver dominates, followed by the stochastic solver.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:correlational· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“It is worth mentioning, however, that none of the grammars for these problems required the synthesizer to discover the bit-vector constants involved in the efficient implementations.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“The subexpression to mutate is chosen uniformly at random, and so the probability of deciding to mutate the boolean condition x ≤ 0 is 1/6.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Given a set of concrete examples {(-1, -4), (-1, -3), (-1, -2), (1, 1), (1, 2)}, Score(e) = exp(-2β), and Score(e ) = exp(-3β), and so e becomes the new candidate with probability exp(-β).”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The symbolic search was the slowest, failing to terminate on 29 of the 57 benchmarks.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“The current set of benchmarks is limited to synthesis of loop-free functions with no optimality criterion;”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“For instance, in the run of the algorithm on the example, although the algorithm enumerated about 200 expressions, only about 80 expressions were stored.”
§ Syntax-Guided Synthesis > D. Enumerative Learning
Strength:plain· not yet calibratedSingle caseTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Our suite includes a range of benchmarks from simple toy problems to nontrivial functions that are difficult to derive by hand.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
In the paper
“This approach provides better running times for most benchmarks in our set, but it can also be more expensive in certain cases.”
§ Syntax-Guided Synthesis > E. Constraint-based Learning
What the sources say
- Not matchedcites [5]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
- Not matched
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“With one exception, the enumerative solver is the fastest for this class of benchmarks, followed by the stochastic solver.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“The Morton benchmarks, which involve the synthesis of a function to compute Morton numbers, are intended as challenge problems, and could not be completed by any of the synthesizers.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Some of the benchmarks can be solved in a few hundredths of a second, whereas others could not be solved by any of our prototype implementations.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“If, on the other hand, e = ITE(x ≤ y, y, x) had been the mutation considered, then Score(e ) = 1, and e would have become the new candidate with probability 1.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:hedged· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“There are 768 integer-valued expressions in the grammar of size six.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✗ Based: failsProbably not a substantial claim. The paper’s conclusions may not depend on it. The paper may give no reason why it holds.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Sketch completed all but 11 of the hd benchmarks, and it was able to synthesize array-search up to size 7.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Of the 48 boolean conditions in the grammar, y ≤ 0 may be chosen with probability 1/48.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:hedged· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
In the paper
“Specifically, we have transcribed all the hacker's delight and integer benchmarks into the input language of the Sketch synthesis system [24].”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
What the sources say
- Not matchedcites [24]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
- Not matched
In the paper
“Many current approaches to synthesis blend induction and deduction [22]; syntax guidance is usually a key ingredient in these approaches.”
§ Syntax-Guided Synthesis > III. INDUCTIVE SYNTHESIS Algorithmic approaches to program synthesis range over a wide spectrum, from deductive synthesis to inductive synthesis.
What the sources say
- Not matchedcites [22]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:correlational· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“In presence of let-expressions, the size directly corresponds to the number of instructions in the corresponding straight-line code, and thus such a metric can be used effectively for applications such as super-optimization.”
§ Syntax-Guided Synthesis > Optimality Criterion:
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Inductive learning is thus a natural fit for the syntax-guided synthesis problem introduced in this paper: the concept class is simply the set L of permissible expressions.”
§ Syntax-Guided Synthesis > III. INDUCTIVE SYNTHESIS Algorithmic approaches to program synthesis range over a wide spectrum, from deductive synthesis to inductive synthesis.
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Finally, it is worth noting that the statement “there exists an expression e in the language generated by a contextfree grammar G such that the formula ϕ[f /e] is valid in a theory T ” cannot be translated to determining the truth of a formula in the theory T , even with additional quantifiers.”
§ Syntax-Guided Synthesis > I. INTRODUCTION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✗ Based: failsProbably not a substantial claim. The paper’s conclusions may not depend on it. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“For example, to optimize the computation of the product of two two-by-two matrices, we can limit the search space to implementations that use only 7 multiplication operations, and such a restriction can be expressed only syntactically.”
§ Syntax-Guided Synthesis > I. INTRODUCTION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✗ Based: failsProbably not a substantial claim. The paper’s conclusions may not depend on it. The paper may give no reason why it holds. It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“First, the user can use the candidate set L to limit the search-space for potential implementations, and this has significant computational benefits for solving the synthesis problem.”
§ Syntax-Guided Synthesis > I. INTRODUCTION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
In the paper
“Many current approaches to synthesis blend induction and deduction [22]; syntax guidance is usually a key ingredient in these approaches.”
§ Syntax-Guided Synthesis > III. INDUCTIVE SYNTHESIS Algorithmic approaches to program synthesis range over a wide spectrum, from deductive synthesis to inductive synthesis.
What the sources say
- Not matchedcites [22]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:correlational· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The top-level expression specified by this grammar is the sum of two identical subexpressions built using arithmetic operators, and such a structure cannot be specified using a standard context-free grammar.”
§ Syntax-Guided Synthesis > Let Expressions in Grammar Productions:
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
None of the sources cited for this claim could be matched to a paper in Crossref, so there is nothing to check it against.
In the paper
“Counterexample-guided inductive synthesis (CEGIS) [16], [24] shown in Figure 1 is perhaps the most popular approach to inductive synthesis today.”
§ Syntax-Guided Synthesis > B. Counterexample-Guided Inductive Synthesis
What the sources say
- Not matchedcites [16]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
- Not matchedcites [24]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:hedged· not yet calibratedTests✓ Asserted: passes✗ Checkable: fails✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. It may be too vague to check against evidence. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“While let-expressions in a specification can be desugared, the same does not hold when they are used in a grammar.”
§ Syntax-Guided Synthesis > Let Expressions in Grammar Productions:
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The answer to our synthesis problem need not be unique: there may be two expressions e 1 and e 2 in the set L of allowed expressions such that both implementations satisfy the correctness specification ϕ.”
§ Syntax-Guided Synthesis > Optimality Criterion:
Load-bearingStrength:hedged· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“For example, every expression in the set L 1 is equivalent to ax+by+c, for integer constants a, b, c.”
§ Syntax-Guided Synthesis > SyGuS Problem Definition:
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Such forms of multi-modal specifications have the potential to make programming more intuitive.”
§ Syntax-Guided Synthesis > I. INTRODUCTION
Tests✓ Asserted: passes✗ Checkable: fails✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim. It may be too vague to check against evidence.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“but the overall trend we observe is that the encoding of the problem space into grammar has a significant impact on performance, although the solvers are often good at mitigating the effect of larger search spaces.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Despite these limitations, the symbolic solver was able to solve many of the benchmarks, providing a lower bound on what can be achieved with a straightforward use of off-the-shelf technology.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“This experiment is not an entirely fair comparison because, although Sketch uses a specialized constraint solver and carefully tuned encodings, the symbolic solver presented in this paper uses a direct encoding of the problem into sequences of constraints and uses Z3, a widely used offthe-shelf SMT solver which is not as aggressively tuned for synthesis problems.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Level d5, on the other extreme, involves a highly unconstrained grammar, so the synthesizer must discover which operators to use in addition to how to connect them together.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
In the paper
“Our algorithm differs from that of Schufza et al. [11] in three ways: (1) we do not attempt to optimize the size of the expression while the super-optimizer does so;”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
What the sources say
- Not matchedcites [11]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“We have some evidence to suggest that the symbolic solver can discover such constants from the full space of 2 32 possible constants with relatively little additional effort.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:hedged· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✗ Based: failsProbably not a substantial claim. The paper’s conclusions may not depend on it. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“If an answer e exists, then the search at size n = |e| is guaranteed to converge.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“We have some evidence that more optimized encodings can make the symbolic approach more competitive, although there are still many problems for which the enumerative approach is more effective.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:hedged· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“In all cases, however, the complexity of the problems derives from the size of the space of possible functions and not from the complexity of checking whether a candidate solution is correct.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✗ Based: failsProbably not a substantial claim. The paper’s conclusions may not depend on it. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“We can also see that nonsymbolic techniques can be effective in exploring spaces of implementations and can surpass symbolic techniques, especially when the problems do not require the synthesizer to derive complex bit-vector constants, which is true for all the bit-vector benchmarks used.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
None of the sources cited for this claim could be matched to a paper in Crossref, so there is nothing to check it against.
In the paper
“CEGIS has close connections to algorithmic debugging using counterexamples [19] and counterexample-guided abstraction refinement (CEGAR) [25].”
§ Syntax-Guided Synthesis > B. Counterexample-Guided Inductive Synthesis
What the sources say
- Not matchedcites [19]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
- Not matchedcites [25]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:correlational· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“However, the order of magnitude of the solution times and the relative complexity of the different approaches on different benchmarks can give us an idea of the relative merits of each of the approaches described earlier.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The problems where the enumerative solver succeeded but Sketch failed were the d5 versions of problems 11, 12, 14 and 15, which suggests that the enumerative solver was better at pruning unnecessary instructions from the grammar.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:hedged· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“For most problems, there are three different levels of grammars numbered d0, d1 and d5; level d0 involves only the instructions necessary for the implementation, so the synthesizer only needs to discover how to connect them together.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
In the paper
“The enumerative learning algorithm [8] adopts a dynamic programming based search strategy that systematically enumerates concepts (expressions) in increasing order of complexity.”
§ Syntax-Guided Synthesis > D. Enumerative Learning
What the sources say
- Not matchedcites [8]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Our prototype implementation of the three approaches to solve this problem is the first attempt to compare and contrast existing algorithms on a common set of benchmarks.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“O V can be implemented as an SMT solver that checks whether ϕ[f /e] is valid modulo the theory T .”
§ Syntax-Guided Synthesis > B. Counterexample-Guided Inductive Synthesis
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Unlike the hd benchmarks where the different grammars for a given benchmark were strict subsets of each other, in this case the encodings AIG and NAND correspond to different representations of the same space of functions.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“None of the implementations were engineered with highperformance in mind, so the exact solution times are not necessarily representative of the best that can be achieved by a particular approach.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim. It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“so although both implementations are immature, these results suggest that it may be easier to derive good pruning rules for the explicit search than an effective fitness function for the stochastic solver.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:hedged· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
In the paper
“The stochastic learning procedure is an adaptation of the algorithm recently used by Schufza et al. [11] for program super-optimization.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
What the sources say
- Not matchedcites [11]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“nevertheless, the benchmarks provide an initial demonstration of the expressiveness of the base formalism and of the relative merits of the individual solution strategies presented earlier.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:boosted· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Grammars can be conveniently used to express a wide range of constraints, and in particular, to bound the depth and/or the size of the desired expression.”
§ Syntax-Guided Synthesis > Set of Candidate Expressions:
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim. It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“On the other hand, for many of these problems the magic constants come from a handful of values such as 1, 0, or 0xffffffff, so it is unnecessary for the enumerative solver to search the space of 2 32 possible bit-vectors.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
In the paper
“(3) since we do not know the expression size n, we run concurrent searches for different values of n, whereas the super-optimizer can use the size of the input program as an upper bound on program size.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
What the sources say
- Not matchedcites [11]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The symbolic solver used for these experiments represents one of many possible approaches to encoding the synthesis problem into a series of constraints.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“For many problems, there are different natural ways to encode the space of desired functions into a grammar, so we are interested in observing the effect of these differences in encoding for the different solvers.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
The authors state this as an assumption.
The free variables in a correctness specification are universally quantified.
“The free variables in the specification are assumed to be universally quantified: a given function f satisfies the above specification if the quantified formula ∀x, y. ϕ 1 holds, or equivalently, if the formula ϕ 1 is valid.”
The paper relies on this without support.
Existing formalization of the SMT problem and the interchange format does not provide a suitable abstraction for capturing syntactic guidance.
“Existing formalization of the SMT problem and the interchange format does not provide a suitable abstraction for capturing the syntactic guidance.”
The paper relies on this without support.
The computational engines used by the various synthesis projects rely on a small set of algorithmic ideas but have evolved independently with no mechanism for comparison, benchmarking, and sharing of back-ends.
“The computational engines used by the various synthesis projects mentioned above rely on a small set of algorithmic ideas, but have evolved independently with no mechanism for comparison, benchmarking, and sharing of back-ends.”
The paper relies on this without support.
The Metropolis-Hastings algorithm guarantees that, in the limit, expressions e are sampled with probability proportional to Score(e).
“The Metropolis-Hastings algorithm guarantees that, in the limit, expressions e are sampled with probability proportional to Score(e).”
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
The cited source doesn’t support the claim as written.
In the citing paper
“This is an approach to software development that aims to produce programs that are guaranteed to be correct with respect to their specifications from the outset, rather than relying on traditional testing and debugging methods to identify and fix errors after the fact.”
From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Alur et al., 2013
Checked by a reasoning model — may be wrong.
Experimental — accuracy not yet measuredThe check wasn’t confident either way, so it gives no verdict — never disputed.
In the citing paper
“EUSolver [Alur et al. 2017], an enumeration-based synthesizer that won the General Track of the most recent SyGuS competition [Alur et al. 2013].”
From Relational program synthesis (2018) · cites this paper as Alur et al. 2013
Experimental — accuracy not yet measured
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
Each contradiction between two passages listed here was confirmed by an independent check.
Stated scores disagree with the example evaluations
MinorUnder the stated cost definition, ITE(x ≤ 0, y, x) fails four of the five listed examples, not two. The stated mutation ITE(0 ≤ y, y, x) fails none, not three.
“Given a set of concrete examples {(-1, -4), (-1, -3), (-1, -2), (1, 1), (1, 2)}, Score(e) = exp(-2β), and Score(e ) = exp(-3β)”
“We define Score(e) to be exp(-βC(e)), where β is a smoothing constant (set by default to 0.5), and the cost function C(e) is the number of concrete examples on which e does not satisfy ϕ.”
Selected condition does not match the stated mutation
MinorThe text says the replacement condition chosen is y ≤ 0, but the resulting expression contains 0 ≤ y. Those are different conditions.
“Of the 48 boolean conditions in the grammar, y ≤ 0 may be chosen with probability 1/48.”
“Thus, the mutation e = ITE(0 ≤ y, y, x) is considered with probability 1/288.”
Citations
Cites
Quinlan, J. R. (1986) · Machine Learning · doi:10.1007/bf00116251 · Cited by 21,439
McKeown (2008) · doi:10.1145/1355734.1355746 · Cited by 8,513
Language identification in the limit
Gold, E. M. (1967) · Information and Control · doi:10.1016/s0019-9958(67)91165-5 · Cited by 3,572
Angluin, D. (1988) · Machine Learning · doi:10.1023/a:1022821128753 · Cited by 1,918
Satisfiability Modulo Theories
Barrett, C. W., Sebastiani, R., Seshia, S., et al. (2009) · Handbook of Satisfiability · doi:10.3233/978-1-58603-929-5-825 · Cited by 1,909
Self-citationGude, N. S., Koponen, T., Pettit, J., Pfaff, B., Casado, M., McKeown, N., & Shenker, S. J. (2008) · ACM SIGCOMM Computer Communication Review · doi:10.1145/1384609.1384625 · Cited by 1,447
Satisfiability Modulo Theories
Barrett, C., & Tinelli, C. (2018) · Springer eBooks · doi:10.1007/978-3-319-10575-8_11 · Cited by 1,148
Shapiro, E. Y. (1983) · doi:10.7551/mitpress/1192.001.0001 · Cited by 1,085
Counterexample-guided abstraction refinement for symbolic model checking
Clarke, E. M., Grümberg, O., Jha, S., Lu, Y., & Veith, H. (2003) · Journal of the ACM · doi:10.1145/876638.876643 · Cited by 997
(2010) · doi:10.5555/1855711.1855728 · Cited by 970
Flagged first, then by citations
Research works printed but not linked: 4
- pox, 2011, OpenFlow Controller
- shenker, 2011, The Future of Networking and the Past of Protocols"
- 0, F OpenFlow Controller
- handigol, 2009, Plug-n-Serve Load-balancing Web Traffic Using OpenFlow
Cited by
Sorted by citations
Items 201–300 of 656
von Essen, C., & Jobstmann, B. (2015) · Formal Methods in System Design · doi:10.1007/s10703-015-0223-6 · Cited by 18
Verified lifting of stencil computations
Kamil, S. A., Cheung, A., Itzhaky, S., & Solar-Lezama, A. (2016) · ACM SIGPLAN Notices · doi:10.1145/2980983.2908117 · Cited by 18
Self-citationAI Evaluation: past, present and futurePreprint
Hernández‐Orallo, J. (2014) · arXiv (Cornell University) · doi:10.48550/arxiv.1408.6908 · Cited by 18
Wang, Y., Wang, X., & Dillig, I. (2018) · Proceedings of the ACM on Programming Languages · doi:10.1145/3276525 · Cited by 17
Blicha, M., Britikov, K., & Sharygina, N. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-37703-7_10 · Cited by 17
Regression-Free Synthesis for Concurrency
Černý, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., & Tarrach, T. (2014) · Lecture notes in computer science · doi:10.1007/978-3-319-08867-9_38 · Cited by 17
Ardeshiricham, A., Takashima, Y., Gao, S., & Kastner, R. (2019) · ACM SIGSAC Conference on Computer and Communications Security (CCS) · doi:10.1145/3319535.3354246 · Cited by 17
Feedback-driven semi-supervised synthesis of program transformations
Gao, X. Y., Barke, S., Radhakrishna, A., Soares, G., Gulwani, S., Leung, A., Nagappan, N., & Tiwari, A. (2020) · Proceedings of the ACM on Programming Languages · doi:10.1145/3428287 · Cited by 17
Word level property directed reachability
K, H. G. V., Fedyukovich, G., & Gurfinkel, A. (2020) · doi:10.1145/3400302.3415708 · Cited by 17
Recent Advances in Intelligent Source Code Generation: A Survey on Natural Language Based Studies
Yang, C., Liu, Y., & Yin, C. (2021) · Entropy · doi:10.3390/e23091174 · Cited by 20
Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation
Yoon, Y., Lee, W., & Yi, K. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3591288 · Cited by 17
High-Level Abstractions for Simplifying Extended String Constraints in SMT
Reynolds, A., Nötzli, A., Barrett, C., & Tinelli, C. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-25543-5_2 · Cited by 17
Testing Dafny (experience paper)
Irfan, A., Porncharoenwase, S., Rakamarić, Z., Rungta, N., & Torlak, E. (2022) · ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) · doi:10.1145/3533767.3534382 · Cited by 16
Self-citationGenerative AI for Software Development: A Family of Studies on Code Generation
Dakhel, A. M., Nikanjam, A., Khomh, F., Desmarais, M. C., & Washizaki, H. (2024) · Springer eBooks · doi:10.1007/978-3-031-55642-5_7 · Cited by 18
Dinesh, S., Madhusudan, P., & Fletcher, C. W. (2024) · IEEE Symposium on Security and Privacy (S&P) · doi:10.1109/sp54263.2024.00180 · Cited by 17
Automatic Completion of Distributed Protocols with Symmetry
Rajeev Alur, A., Raghothaman, M., Stergiou, C. L., Tripakis, S., & Udupa, A. (2015) · Lecture notes in computer science · doi:10.1007/978-3-319-21668-3_23 · Cited by 16
Self-citationZhang, H., Trippel, C., Manerkar, Y. A., Gupta, A., Martonosi, M., & Malik, S. (2018) · Formal Methods in Computer-Aided Design · doi:10.23919/fmcad.2018.8603015 · Cited by 16
Raza, M., & Gulwani, S. (2020) · ACM SIGMOD International Conference on Management of Data (SIGMOD) · doi:10.1145/3318464.3380608 · Cited by 16
Speeding up constraint-based program repair using a search-based technique
Yi, J., & Ismayilzada, E. (2022) · Information and Software Technology · doi:10.1016/j.infsof.2022.106865 · Cited by 16
Neural-Guided Symbolic Regression with Asymptotic ConstraintsPreprint
Li, L., Fan, M., Singh, R., & Riley, P. F. (2019) · arXiv (Cornell University) · doi:10.48550/arxiv.1901.07714 · Cited by 27
Self-citationModular divide-and-conquer parallelization of nested loops
Farzan, A., & Nicolet, V. (2019) · Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation · doi:10.1145/3314221.3314612 · Cited by 16
Perfect Is the Enemy of Good: Best-Effort Program Synthesis
Peleg, H., & Polikarpova, N. (2020) · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · doi:10.4230/lipics.ecoop.2020.2 · Cited by 15
Using Reactive Synthesis: An End-to-End Exploratory Case Study
Ma’ayan, D., & Maoz, S. (2023) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse48619.2023.00071 · Cited by 15
Simplifying Mixed Boolean-Arithmetic Obfuscation by Program Synthesis and Term Rewriting
Lee, J. W., & Lee, W. (2023) · ACM SIGSAC Conference on Computer and Communications Security (CCS) · doi:10.1145/3576915.3623186 · Cited by 15
Alchemist: Learning Guarded Affine Functions
Saha, S., Garg, P., & Madhusudan, P. (2015) · Lecture notes in computer science · doi:10.1007/978-3-319-21690-4_26 · Cited by 15
An SMT Based Method for Optimizing Arithmetic Computations in Embedded Software Code
Eldib, H., & Wang, C. (2014) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/tcad.2014.2341931 · Cited by 15
A multi-paradigm language for reactive synthesis
Filippidis, I. F., Murray, R. M., & Holzmann, G. J. (2016) · Electronic Proceedings in Theoretical Computer Science · doi:10.4204/eptcs.202.6 · Cited by 15
Towards efficient and effective automatic program repair
Le, X.-B. D. (2016) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/2970276.2975934 · Cited by 15
Wang, C., & Schaumont, P. R. (2017) · ACM SIGLOG News · doi:10.1145/3090064.3090071 · Cited by 15
Decidable Synthesis of Programs with Uninterpreted Functions
Krogmeier, P., Mathur, U., Murali, A., Madhusudan, P., & Viswanathan, M. (2020) · Lecture notes in computer science · doi:10.1007/978-3-030-53291-8_32 · Cited by 15
Program Repair for Hyperproperties
Bonakdarpour, B., & Finkbeiner, B. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-31784-3_25 · Cited by 15
Knoth, T., Wang, D., Reynolds, A., Hoffmann, J., & Polikarpova, N. (2020) · Proceedings of the ACM on Programming Languages · doi:10.1145/3408988 · Cited by 15
Syntax-Guided Quantifier Instantiation
Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., & Tinelli, C. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-72013-1_8 · Cited by 15
Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzing
Muduli, S. K., & Roy, S. (2022) · Proceedings of the ACM on Programming Languages · doi:10.1145/3563332 · Cited by 15
Synthesis of Recursive ADT Transformations from Reusable Templates
Inala, J. P., Polikarpova, N., Qiu, X., Lerner, B. S., & Solar-Lezama, A. (2017) · Lecture notes in computer science · doi:10.1007/978-3-662-54577-5_14 · Cited by 15
Self-citationAutogenerating Fast Packet-Processing Code Using Program Synthesis
Gao, X., Kim, T., Varma, A. K., Sivaraman, A., & Narayana, S. (2019) · ACM Workshop on Hot Topics in Networks (HotNets) · doi:10.1145/3365609.3365858 · Cited by 15
Programming with a read-eval-synth loop
Peleg, H., Gabay, R., Itzhaky, S., & Yahav, E. (2020) · Proceedings of the ACM on Programming Languages · doi:10.1145/3428227 · Cited by 15
Inductive Synthesis for Probabilistic Programs Reaches New Horizons
Andriushchenko, R., Češka, M., Junges, S., & Katoen, J.-P. (2021) · Lecture notes in computer science · doi:10.26226/morressier.604907f41a80aac83ca25cf1 · Cited by 16
Fremont, D. J., Rabe, M. N., & Seshia, S. A. (2017) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v31i1.11138 · Cited by 14
Self-citationAlive-Infer: data-driven precondition inference for peephole optimizations in LLVM
Menendez, D., & Nagarakatte, S. (2017) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3062341.3062372 · Cited by 14
Bit-Precise Reasoning via Int-Blasting
Zohar, Y., Irfan, A., Mann, M., Niemetz, A., Nötzli, A., Preiner, M., Reynolds, A., Barrett, C., & Tinelli, C. (2022) · Lecture notes in computer science · doi:10.1007/978-3-030-94583-1_24 · Cited by 14
Solving Infinite-State Games via Acceleration
Heim, P., & Dimitrova, R. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3632899 · Cited by 14
VeCoGen: Automating Generation of Formally Verified C Code With Large Language Models
Sevenhuijsen, M., Etemadi, K., & Nyberg, M. (2025) · IEEE/ACM International Conference on Formal Methods in Software Engineering (FormaliSE) · doi:10.1109/formalise66629.2025.00017 · Cited by 22
Using Program Synthesis for Program Analysis
David, C., Kroening, D., & Lewis, M. (2015) · Lecture notes in computer science · doi:10.1007/978-3-662-48899-7_34 · Cited by 14
Systematic Generation of Non-equivalent Expressions for Relational Algebra
Wang, K., Sullivan, A., Koukoutos, M., Marinov, D., & Sarfraz Khurshid, D. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-91271-4_8 · Cited by 14
Benchmarking Multimodal Regex Synthesis with Complex Structures
Ye, X., Chen, Q., Dillig, I., & Durrett, G. (2020) · Proceedings of the conference - Association for Computational Linguistics. Meeting · doi:10.18653/v1/2020.acl-main.541 · Cited by 14
Generalizable synthesis through unification
Ji, R., Xia, J., Xiong, Y., & Hu, Z. (2021) · Proceedings of the ACM on Programming Languages · doi:10.1145/3485544 · Cited by 14
UDF to SQL translation through compositional lazy inductive synthesis
Zhang, G., Xu, Y., Shen, X., & Dillig, I. (2021) · Proceedings of the ACM on Programming Languages · doi:10.1145/3485489 · Cited by 14
Induction duality: primal-dual search for invariants
Padon, O., Wilcox, J. R., Koenig, J. R., McMillan, K. L., & Aiken, A. (2022) · Proceedings of the ACM on Programming Languages · doi:10.1145/3498712 · Cited by 14
Vector instruction selection for digital signal processors using program synthesis
Ahmad, M. B. S., Root, A. J., Adams, A., Kamil, S. A., & Cheung, A. (2022) · International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) · doi:10.1145/3503222.3507714 · Cited by 14
Hierarchical Contract-Based Synthesis for Assurance Cases
Wang, T. E., Daw, Z., Nuzzo, P., & Pinto, A. (2022) · Lecture notes in computer science · doi:10.1007/978-3-031-06773-0_9 · Cited by 14
Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs
Goharshady, A. K., Hitarth, S., Mohammadi, F., & Motwani, H. J. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3586052 · Cited by 19
Synthesizing Environment Invariants for Modular Hardware Verification
Zhang, H., Yang, W., Fedyukovich, G., Gupta, A., & Malik, S. (2020) · Lecture notes in computer science · doi:10.1007/978-3-030-39322-9_10 · Cited by 14
Navigating Confidentiality in Test Automation: A Case Study in LLM Driven Test Data Generation
Karmarkar, H., Agrawal, S., Chauhan, A., & Shete, P. (2024) · IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER) · doi:10.1109/saner60148.2024.00041 · Cited by 15
DeCastro, J., & Kress‐Gazit, H. (2016) · International Conference on Hybrid Systems: computation and control · doi:10.1145/2883817.2883832 · Cited by 13
Counterexample-Guided Partial Bounding for Recursive Function Synthesis
Farzan, A., & Nicolet, V. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-81685-8_39 · Cited by 13
A Max-SMT Superoptimizer for EVM handling Memory and Storage
Albert, E., Gordillo, P., Hernández-Cerezo, A., & Rubio, A. (2022) · Lecture notes in computer science · doi:10.1007/978-3-030-99524-9_11 · Cited by 13
Multi-phase invariant synthesis
Riley, D., & Fedyukovich, G. (2022) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/3540250.3549166 · Cited by 13
Learning to Synthesize Relational Invariants
Wang, J., & Wang, C. (2022) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/3551349.3556942 · Cited by 13
Explainable Program Synthesis by Localizing Specifications
Nazari, A., Huang, Y., Samanta, R., Radhakrishna, A., & Raghothaman, M. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3622874 · Cited by 13
Self-citationConnecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation
Nguyen, T. H., Weimer, W. R., Kapur, D., & Forrest, S. (2017) · Lecture notes in computer science · doi:10.1007/978-3-662-54577-5_17 · Cited by 13
Counterexample Guided Synthesis of Switched Controllers for Reach-While-Stay PropertiesPreprint
Ravanbakhsh, H., & Sankaranarayanan, S. (2015) · arXiv (Cornell University) · doi:10.48550/arxiv.1505.01180 · Cited by 13
Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems
Dalrymple, D. "., Skalse, J., Bengio, Y., Russell, S., Tegmark, M., Seshia, S., Omohundro, S., Szegedy, C., Goldhaber, B., Ammann, N., et al. (2024) · arXiv · doi:10.48550/arxiv.2405.06624 · Cited by 12
Self-citationAn SMT based method for optimizing arithmetic computations in embedded software code
Eldib, H., & Wang, C. (2013) · Formal Methods in Computer-Aided Design · doi:10.1109/fmcad.2013.6679401 · Cited by 12
Hydra: Generalizing Peephole Optimizations with Program Synthesis
Mukherjee, M., & Regehr, J. D. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3649837 · Cited by 12
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Fakhoury, S., Kuppe, M. A., Lahiri, S. K., Ramananandro, T., & Swamy, N. (2025) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse55347.2025.00173 · Cited by 17
Precise piecewise affine models from input-output data
Rajeev Alur, A., & Singhania, N. (2014) · ACM International Conference on Embedded Software (EMSOFT) · doi:10.1145/2656045.2656064 · Cited by 12
Complexity and information in invariant inference
Feldman, Y. M. Y., Immerman, N., Sagiv, M., & Shoham, S. (2019) · Proceedings of the ACM on Programming Languages · doi:10.1145/3371073 · Cited by 12
Example-guided synthesis of relational queries
Thakkar, A., Naik, A., Sands, N., Rajeev Alur, A., Naik, M., & Raghothaman, M. (2021) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3453483.3454098 · Cited by 12
Self-citationMurxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers
Niemetz, A., Preiner, M., & Barrett, C. (2022) · Lecture notes in computer science · doi:10.1007/978-3-031-13188-2_5 · Cited by 12
Programming-by-Demonstration for Long-Horizon Robot Tasks
Patton, N., Rahmani, K., Missula, M., Biswas, J., & Dillig, I. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3632860 · Cited by 12
Invited - Specification and modeling for systems-on-chip security verification
Malik, S., & Subramanyan, P. (2016) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/2897937.2911991 · Cited by 12
SyGuS Techniques in the Core of an SMT Solver
Reynolds, A., & Tinelli, C. (2017) · Electronic Proceedings in Theoretical Computer Science · doi:10.4204/eptcs.260.8 · Cited by 12
Solver-Based Sketching of Alloy Models Using Test Valuations
Wang, K., Sullivan, A., Marinov, D., & Sarfraz Khurshid, D. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-91271-4_9 · Cited by 12
Datatypes with Shared Selectors
Reynolds, A., Viswanathan, A., Barbosa, H., Tinelli, C., & Barrett, C. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-94205-6_39 · Cited by 12
Clock Bound Repair for Timed Systems
Kölbl, M., Leue, S., & Wies, T. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-25540-4_5 · Cited by 12
Clavière, A., Dutta, S., & Sankaranarayanan, S. (2019) · Proceedings of the International Conference on Automated Planning and Scheduling · doi:10.1609/icaps.v29i1.3555 · Cited by 12
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
Zhang, H., Gupta, A., & Malik, S. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-67067-2_15 · Cited by 12
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
Mann, M., Irfan, A., Griggio, A., Padon, O., & Barrett, C. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-72016-2_7 · Cited by 12
Gradient-Descent for Randomized Controllers Under Partial Observability
Heck, L., Spel, J., Junges, S., Moerman, J., & Katoen, J.-P. (2022) · Lecture notes in computer science · doi:10.1007/978-3-030-94583-1_7 · Cited by 12
Modeling Undefined Behaviour Semantics for Checking Equivalence Across Compiler Optimizations
Dahiya, M., & Bansal, S. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-70389-3_2 · Cited by 12
Generalized Program Sketching by Abstract Interpretation and Logical Abduction
Dimovski, A. S. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-44245-2_11 · Cited by 11
Scalable Bit-Blasting with Abstractions
Niemetz, A., Preiner, M., & Zohar, Y. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-65627-9_9 · Cited by 11
EdSynth: Synthesizing API Sequences with Conditionals and Loops
Yang, Z., Hua, J., Wang, K., & Sarfraz Khurshid, D. (2018) · IEEE International Conference on Software Testing, Verification and Validation (ICST) · doi:10.1109/icst.2018.00025 · Cited by 11
Regular Model Checking Revisited
Lin, A. W., & Rümmer, P. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-91384-7_6 · Cited by 11
Model-guided synthesis of inductive lemmas for FOL with least fixpoints
Murali, A., Peña, L., Blanchard, E., Löding, C., & Madhusudan, P. (2022) · Proceedings of the ACM on Programming Languages · doi:10.1145/3563354 · Cited by 11
A Case for Synthesis of Recursive Quantum Unitary Programs
Deng, H., Tao, R., Peng, Y., & Wu, X. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3632901 · Cited by 14
Combining the logical and the probabilistic in program analysis
Zhang, X., Si, X., & Naik, M. (2017) · ACM SIGPLAN International Workshop on Machine Learning and Programming Languages (MAPL) · doi:10.1145/3088525.3088563 · Cited by 11
Strategy Representation by Decision Trees with Linear Classifiers
Ashok, P., Brázdil, T., Chatterjee, K., Křetínský, J., Lampert, C. H., & Toman, V. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-30281-8_7 · Cited by 11
On Strings in Software Model Checking
Hojjat, H., Rümmer, P., & Shamakhi, A. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-34175-6_2 · Cited by 11
Extending enumerative function synthesis via SMT-driven classification
Barbosa, H., Reynolds, A., Larraz, D., & Tinelli, C. (2019) · Formal Methods in Computer-Aided Design · doi:10.23919/fmcad.2019.8894267 · Cited by 11
Phased synthesis of divide and conquer programs
Farzan, A., & Nicolet, V. (2021) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3453483.3454089 · Cited by 11
Toward tool support for interactive synthesis
Barman, S., Bodík, R., Chandra, S., Torlak, E., Bhattacharya, A., & Culler, D. (2015) · ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!) · doi:10.1145/2814228.2814235 · Cited by 11
Self-citationWebRelate: integrating web data with spreadsheets using examples
Inala, J. P., & Singh, R. (2017) · Proceedings of the ACM on Programming Languages · doi:10.1145/3158090 · Cited by 11
Self-citationGulwani, S. (2017) · International Symposium on Principles and Practice of Declarative Programming (PPDP) · doi:10.1145/3131851.3131853 · Cited by 11
Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
Inala, J. P., Singh, R., & Solar-Lezama, A. (2016) · Lecture notes in computer science · doi:10.1007/978-3-319-40970-2_19 · Cited by 10
Self-citationDesign Understanding: From Logic to Specification
Fey, G., Ghasempouri, T., Jacobs, S., Martino, G., Raik, J., & Riener, H. (2018) · IFIP/IEEE International Conference on Very Large Scale Integration · doi:10.1109/vlsi-soc.2018.8644732 · Cited by 10
Verifiable and Interpretable Reinforcement Learning through Program Synthesis
Verma, A. (2019) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v33i01.33019902 · Cited by 10
Automating Modular Verification of Secure Information Flow
Pick, L., Fedyukovich, G., & Gupta, A. (2020) · doi:10.34727/2020/isbn.978-3-85448-042-6_23 · Cited by 10
A large-scale benchmark for few-shot program induction and synthesis
Alet, F., Lopez-Contreras, J., Koppel, J., Nye, M., Solar-Lezama, A., Lozano‐Pérez, T., Kaelbling, L. P., & Tenenbaum, J. (2021) · DSpace@MIT (Massachusetts Institute of Technology) · Cited by 10
Self-citation
Metadata
- Authors
- Alur, R., Bodik, R., Juniwal, G., Martin, M. M. K., Raghothaman, M., Seshia, S. A., Singh, R., Solar-Lezama, A., Torlak, E., & Udupa, A.
- Affiliations
- University of California, Berkeley (US)
- University of Pennsylvania (US)
- Massachusetts Institute of Technology (US)
- Venue
- 2013 Formal Methods in Computer-Aided Design
- Publisher
- IEEE
- Published
- 2013-10
- Pages
- 1-8
- OpenAlex
- W2094878426
- Cited by
- 656
- References
- 50
- Citations by year
- 2026: 29 · 2025: 45 · 2024: 48 · 2023: 55 · 2022: 49 · 2021: 65 · 2020: 64 · 2019: 63 · 2018: 61 · 2017: 58 · 2016: 54 · 2015: 37 · 2014: 25 · 2013: 3
- FWCI
- 25.24
- Type
- conference paper
- Language
- en
- Open access
- green
- hdl.handle.net
- Licence
- cc-by-nc-sa
- Locations
- Formal Methods in Computer-Aided Design (publishedVersion)
- DSpace@MIT (Massachusetts Institute of Technology) (submittedVersion, cc-by-nc-sa)
- eScholarship (California Digital Library) (submittedVersion)
- Other univ. web domain
- Funders
- National Science Foundation (1138996)
- Topics
- Physical Sciences › Computer Science › Software › Logic, programming, and type systems
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
- Keywords
- syntax-guided synthesis, program synthesis, grammar, background theory, program optimization
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
A language model drew the claims from the paper on 2026-11-05, under version 3 of the claim definition (model deepseek-v4.1-flash, prompt extract-v3).
A second model labelled each claim on 2026-11-05 (model jev-1.13-20260917, definition revision gold-guideline-v0.2).
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
