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 401–500 of 656
Petablox: Large-Scale Software Analysis and Analytics Using Datalog
Naik, M. (2020) · Cited by 5
Software Ticks Need No Specifications
Reichenbach, C. (2021) · IEEE/ACM International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER) · doi:10.1109/icse-nier52604.2021.00021 · Cited by 5
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities
Itzhaky, S., Peleg, H., Polikarpova, N., Rowe, R. N. S., & Sergey, I. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-81685-8_5 · Cited by 5
Phothilimthana, P. M., Thakur, A., Bodík, R., & Dhurjati, D. (2016) · ACM SIGOPS Operating Systems Review · doi:10.1145/2954680.2872387 · Cited by 5
Portability and Explainability of Synthesized Formula-based Heuristics
Bulitko, V. V., Wang, S., Stevens, J., & Lelis, L. H. S. (2022) · Proceedings of the International Symposium on Combinatorial Search · doi:10.1609/socs.v15i1.21749 · Cited by 5
Constraint-Based Synthesis of Coupling Proofs
Albarghouthi, A., & Hsu, J. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-96145-3_18 · Cited by 5
A Decidable Fragment of Second Order Logic With Applications to SynthesisPreprint
Madhusudan, P., Mathur, U., Saha, S., & Viswanathan, M. (2017) · arXiv (Cornell University) · doi:10.4230/lipics.csl.2018.31 · Cited by 5
CounterExample Guided Neural SynthesisPreprint
Polgreen, E., Abboud, R., & Kroening, D. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2001.09245 · Cited by 10
Neural Program Synthesis with a Differentiable FixerPreprint
Balog, M., Singh, R., Maniatis, P., & Sutton, C. A. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2006.10924 · Cited by 5
Self-citationReinforcement learning with learned gadgets to tackle hard quantum problems on real hardware
Kundu, A., & Sarra, L. (2026) · Communications Physics · doi:10.1038/s42005-025-02475-6 · Cited by 15
Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
Johnson, K. J. C., Krishnan, R., Reps, T., & D’Antoni, L. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3689744 · Cited by 4
Practical formal techniques and tools for developing LLVM’s peephole optimizations
Menendez, D. (2018) · doi:10.7282/t3ff3wk4 · Cited by 4
Jacindha, S., Abishek, G. D., & Vasuki, P. (2022) · Lecture notes in electrical engineering · doi:10.1007/978-981-16-8484-5_39 · Cited by 4
Solving Constrained Horn Clauses over Algebraic Data Types
Zavalía, L., Chernigovskaia, L., & Fedyukovich, G. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-24950-1_16 · Cited by 4
Synthesizing Trajectory Queries from Examples
Mell, S., Bastani, F., Zdancewic, S., & Bastani, O. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-37706-8_23 · Cited by 4
Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
Akshay, S., Chakraborty, S., Goharshady, A. K., Govind, R., Motwani, H. J., & Varanasi, S. T. (2024) · EPiC series in computing · doi:10.29007/njph · Cited by 4
Syntax-Guided Automated Program Repair for Hyperproperties
Beutner, R., Hsu, T.-H., Bonakdarpour, B., & Finkbeiner, B. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-65633-0_1 · Cited by 4
Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
Nagy, S., Kim, J., Reps, T., & D’Antoni, L. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3689715 · Cited by 4
Bridging the Gap Between General-Purpose and Domain-Specific Compilers with Synthesis
Cheung, A., Kamil, S. A., & Solar-Lezama, A. (2015) · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · doi:10.4230/lipics.snapl.2015.51 · Cited by 4
Self-citationLearning Implicitly with Noisy Data in Linear Arithmetic
Rader, A. P., Mocanu, I. G., Belle, V., & Juba, B. (2021) · International Joint Conference on Artificial Intelligence · doi:10.24963/ijcai.2021/195 · Cited by 4
Adaptive restarts for stochastic synthesis
Koenig, J. R., Padon, O., & Aiken, A. (2021) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3453483.3454071 · Cited by 4
Condition Synthesis Realizability via Constrained Horn Clauses
Rothenberg, B.-C., Grümberg, O., Vizel, Y., & Singher, E. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-33170-1_23 · Cited by 4
Iterative genetic improvement: Scaling stochastic program synthesis
Yuan, Y., & Banzhaf, W. (2023) · Artificial Intelligence · doi:10.1016/j.artint.2023.103962 · Cited by 4
Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis
Parsert, J., & Polgreen, E. (2024) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v38i9.28938 · Cited by 4
Lifting Micro-Update Models from RTL for Formal Security Analysis
Godbole, A., Cheang, K., Manerkar, Y. A., & Seshia, S. A. (2024) · International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) · doi:10.1145/3620665.3640418 · Cited by 4
Self-citationSingh, R., & Solar-Lezama, A. (2016) · Formal Methods in Computer-Aided Design · doi:10.5555/3077629.3077661 · Cited by 4
Self-citationSynthesis of Algorithm Considering Communication Structure of Distributed/Parallel Computing
Miyasaka, Y., Mittal, A., & Fujita, M. (2019) · International Symposium on Quality Electronic Design (ISQED) · doi:10.1109/isqed.2019.8697224 · Cited by 4
Harel, D., Marron, A., Rosenfeld, A., Vardi, M. Y., & Weiss, G. (2019) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v33i01.33019770 · Cited by 4
CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories
Kallat, F., Schäfer, T., & Vasileva, A. (2019) · Electronic Proceedings in Theoretical Computer Science · doi:10.4204/eptcs.301.7 · Cited by 4
Cognification of Program Synthesis—A Systematic Feature-Oriented Analysis and Future Direction
Subahi, A. F. (2020) · Computers · doi:10.3390/computers9020027 · Cited by 4
Synthesis of infinite-state systems with random behavior
Katis, A., Fedyukovich, G., Chen, J. Y., Greve, D., Rayadurgam, S., & Whalen, M. W. (2020) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/3324884.3416586 · Cited by 4
On solving quantified bit-vector constraints using invertibility conditions
Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., & Tinelli, C. (2021) · Formal Methods in System Design · doi:10.1007/s10703-020-00359-9 · Cited by 4
Bridging Arrays and ADTs in Recursive Proofs
Fedyukovich, G., & Ernst, G. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-72013-1_2 · Cited by 4
Trident: Controlling Side Effects in Automated Program Repair
Parasaram, N., Barr, E. T., & Mechtaev, S. (2021) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2021.3124323 · Cited by 4
PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency
Norman, C., Godbole, A., & Manerkar, Y. A. (2023) · International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) · doi:10.1145/3582016.3582056 · Cited by 4
Programming by Example Made Easy
Wu, J., Wei, L., Jiang, Y., Cheung, S.-C., Ren, L., & Xu, C. (2023) · ACM Transactions on Software Engineering and Methodology · doi:10.1145/3607185 · Cited by 4
FudgeFactor: Syntax-Guided Synthesis for Accurate RTL Error Localization and Correction
Becker, A., Maksimovic, D., Novo, D., Ewaida, M., Veneris, A. G., Jobstmann, B., & Ienne, P. (2015) · Lecture notes in computer science · doi:10.1007/978-3-319-26287-1_16 · Cited by 4
Lu, Y., Chaudhuri, S., Jermaine, C., & Melski, D. (2018) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1145/3180155.3180190 · Cited by 4
Learning Guided Enumerative Synthesis for Superoptimization
Singh, S., Zhang, M., & Sarfraz Khurshid, D. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-30923-7_10 · Cited by 4
On (I/O)-Aware Good-For-Games Automata
Faran, R., & Kupferman, O. (2020) · Lecture notes in computer science · doi:10.1007/978-3-030-59152-6_9 · Cited by 4
QBF Solving by Counterexample-guided ExpansionPreprint
Bloem, R., Braud-Santoni, N., & Hadžić, V. (2016) · arXiv (Cornell University) · doi:10.48550/arxiv.1611.01553 · Cited by 4
DevReplay: Automatic Repair with Editable Fix PatternPreprint
Ueda, Y., Ishio, T., Ihara, A., & Matsumoto, K. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2005.11040 · Cited by 4
Robot Action Selection Learning via Layered Dimension Informed Program SynthesisPreprint
Holtz, J., Guha, A., & Biswas, J. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2008.04133 · Cited by 4
Active Perception and Control from PrSTL SpecificationsPreprint
da Silva, R. R., Kurtz, V., & Lin, H. (2021) · arXiv (Cornell University) · doi:10.48550/arxiv.2111.02226 · Cited by 4
Automated Discovery of Simulation Between Programs
Fedyukovich, G., Gurfinkel, A., & Sharygina, N. (2014) · doi:10.21236/ada613949 · Cited by 4
Gröbner Bases for Boolean Function Minimization
Faroß, N., & Schwarz, S. (2025) · Mathematics in Computer Science · doi:10.1007/s11786-025-00602-8 · Cited by 3
Golem: a flexible and efficient solver for constrained Horn clauses
Blicha, M., Britikov, K., & Sharygina, N. (2025) · Formal Methods in System Design · doi:10.1007/s10703-025-00470-9 · Cited by 3
Synthesizing MILP Constraints for Efficient and Robust Optimization
Wang, J., Gupta, A., & Wang, C. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3591298 · Cited by 3
Optimizing Homomorphic Evaluation Circuits by Program Synthesis and Time-bounded Exhaustive Search
Lee, D., Lee, W., Oh, H., & Yi, K. (2023) · ACM Transactions on Programming Languages and Systems · doi:10.1145/3591622 · Cited by 3
Towards Safer Heuristics With XPlain
Karimi, P., Pirelli, S., Kakarla, S. K. R., Beckett, R., Segarra, S., Li, B., Namyar, P., & Arzani, B. (2024) · ACM Workshop on Hot Topics in Networks (HotNets) · doi:10.1145/3696348.3696884 · Cited by 5
Innovating Education and Entrepreneurship Through Computational Thinking
Tariq, M. U. (2024) · Advances in business strategy and competitive advantage book series · doi:10.4018/979-8-3693-9486-1.ch001 · Cited by 3
Satisfiability Modulo User Propagators
Fazekas, K., Niemetz, A., Preiner, M., Kirchweger, M., Szeider, S., & Biere, A. (2024) · Journal of Artificial Intelligence Research · doi:10.1613/jair.1.16163 · Cited by 3
Dar, M. D., Lorch, R., Sadeghi, A., Sorcigli, V., Gollier, H., Tinelli, C., Vanhoef, M., & Chowdhury, O. (2025) · IEEE Symposium on Security and Privacy (S&P) · doi:10.1109/sp61157.2025.00211 · Cited by 3
Automating Repetitive Tasks for the Masses
Gulwani, S. (2014) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · doi:10.1145/2676726.2682621 · Cited by 3
Synthesizing Mutable Configurations: Setting up Systems for Success
Nelson, T., Danas, N., Giannakopoulos, T., & Krishnamurthi, S. (2019) · IEEE/ACM International Conference on Automated Software Engineering Workshops (ASEW) · doi:10.1109/asew.2019.00034 · Cited by 3
Towards automated input generation for sketching alloy models
Jovanovic, A., & Sullivan, A. (2022) · IEEE/ACM International Conference on Formal Methods in Software Engineering (FormaliSE) · doi:10.1145/3524482.3527651 · Cited by 3
Understanding the Power of Evolutionary Computation for GPU Code Optimization
Liou, J.-Y., Awan, M. G., Hofmeyr, S. A., Forrest, S., & Wu, C.-J. (2022) · IEEE International Symposium on Workload Characterization · doi:10.1109/iiswc55918.2022.00025 · Cited by 3
Experiments on Infinite Model Finding in SMT Solving
Parsert, J., Brown, C. E., Janota, M., & Kaliszyk, C. (2023) · EPiC series in computing · doi:10.29007/slrm · Cited by 3
An Interactive SMT Tactic in Coq using Abductive Reasoning
Barbosa, H., Keller, C., Reynolds, A., Viswanathan, A., Tinelli, C., & Barrett, C. (2023) · EPiC series in computing · doi:10.29007/432m · Cited by 3
Synthesizing Device Drivers with Ghost Writer
Wang, B., Noorafshan, S., Achermann, R., & Seltzer, M. (2023) · Workshop on Programming Languages and Operating Systems (PLOS) · doi:10.1145/3623759.3624545 · Cited by 3
Survey of intelligent program synthesis techniques
Zhou, B., & Ding, G. (2023) · International Conference on Algorithms, High Performance Computing and Artificial Intelligence (AHPCAI) · doi:10.1117/12.3011627 · Cited by 3
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
Elad, N., Padon, O., & Shoham, S. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3632875 · Cited by 3
Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
Kamp, M., & Philippsen, M. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-67067-2_16 · Cited by 3
Algebra-Based Synthesis of Loops and Their Invariants (Invited Paper)
Humenberger, A., & Kovács, L. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-67067-2_2 · Cited by 3
Network Traffic Classification by Program Synthesis
Shi, L., Li, Y., Loo, B. T., & Rajeev Alur, A. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-72016-2_23 · Cited by 3
Satisfiability and Synthesis Modulo Oracles
Polgreen, E., Reynolds, A., & Seshia, S. A. (2022) · Lecture notes in computer science · doi:10.1007/978-3-030-94583-1_13 · Cited by 3
Self-citationGrafs: declarative graph analytics
Houshmand, F., Lesani, M., & Vora, K. (2021) · Proceedings of the ACM on Programming Languages · doi:10.1145/3473588 · Cited by 3
Synthesizing axiomatizations using logic learning
Krogmeier, P., Lin, Z., Murali, A., & Madhusudan, P. (2022) · Proceedings of the ACM on Programming Languages · doi:10.1145/3563348 · Cited by 3
Synthesising Programs with Non-trivial Constants
Abate, A., Barbosa, H., Barrett, C., David, C., Kesseli, P., Kroening, D., Polgreen, E., Reynolds, A., & Tinelli, C. (2023) · Journal of Automated Reasoning · doi:10.1007/s10817-023-09664-4 · Cited by 3
Human-Driven Genetic Programming for Program Synthesis: A Prototype
Helmuth, T., Frazier, J. G., Shi, Y., & Abdelrehim, A. F. (2023) · Genetic and Evolutionary Computation Conference Companion (GECCO Companion) · doi:10.1145/3583133.3596373 · Cited by 3
Program Synthesis with Best-First Bottom-Up Search
Ameen, S., & Lelis, L. H. S. (2023) · Journal of Artificial Intelligence Research · doi:10.1613/jair.1.14394 · Cited by 3
Generating Programmatic Referring Expressions via Program Synthesis
Huang, J., Smith, C., Bastani, O., Singh, R., Albarghouthi, A., & Naik, M. (2020) · International Conference on Machine Learning · Cited by 3
Self-citationA family of multi-concept program synthesisers in Alloy⁎
Correia, A. R. S., Iyoda, J., & Mota, A. (2020) · Science of Computer Programming · doi:10.1016/j.scico.2020.102536 · Cited by 3
Drill and Join: A Method for Exact Inductive Program Synthesis
Balaniuk, R. (2015) · Lecture notes in computer science · doi:10.1007/978-3-319-17822-6_13 · Cited by 3
Program synthesis for interactive-security systems
Harris, W. R., Jha, S., Reps, T., & Seshia, S. A. (2017) · Formal Methods in System Design · doi:10.1007/s10703-017-0296-5 · Cited by 3
Self-citationMinimal Synthesis of String to String Functions from Examples
Hamza, J., & Kunčak, V. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-11245-5_3 · Cited by 3
A Decidable Logic for Tree Data-Structures with Measurements
Qiu, X., & Wang, Y. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-11245-5_15 · Cited by 3
Fundamental Approaches to Software Engineering
Johnsen, E. B., & Wimmer, M. (2022) · Lecture notes in computer science · doi:10.1007/978-3-030-99429-7 · Cited by 3
Automated Synthesis of Divide and Conquer ParallelismPreprint
Farzan, A., & Nicolet, V. (2017) · arXiv (Cornell University) · doi:10.48550/arxiv.1701.08345 · Cited by 3
Program Synthesis Over Noisy Data with GuaranteesPreprint
Handa, S., & Rinard, M. (2021) · arXiv (Cornell University) · doi:10.48550/arxiv.2103.05030 · Cited by 3
Arellanes, D. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-64626-3_2 · Cited by 2
Inductive Synthesis of Inductive Heap Predicates
Yang, Z., & Sergey, I. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3720420 · Cited by 6
LLM-Driven Neighborhood Search for Efficient Heuristic Design
Xie, Z., Liu, F., Wang, Z., & Zhang, Q. (2025) · IEEE Congress on Evolutionary Computation (CEC) · doi:10.1109/cec65147.2025.11043025 · Cited by 2
LLMs Tackle Meta-analysis: Automating Scientific Hypothesis Generation with Statistical Rigor
Lin, T.-W., Yang, R., Abdeen, Z. U., Sangiovanni-Vincentelli, A. L., Huang, H., & Jin, M. (2025) · Communications in computer and information science · doi:10.1007/978-981-96-8912-5_2 · Cited by 2
Branching Bisimulation Learning
Abate, A., Giacobbe, M., Micheletti, C., & Schnitzer, Y. (2025) · Lecture notes in computer science · doi:10.1007/978-3-031-98685-7_8 · Cited by 2
Vibe Coding: A Multivocal Systematic Mapping Study
Beaulieu, N., Dascalu, S. M., & Hand, E. (2025) · ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing (SNPD) · doi:10.1109/snpd65828.2025.11254176 · Cited by 2
Automatically Engineering Trusted Software: A Research Roadmap
Brun, Y., Chakraborty, S., Goues, C. L., Păsăreanu, C. S., & Singla, A. K. (2026) · ACM Transactions on Software Engineering and Methodology · doi:10.1145/3779132 · Cited by 2
AutoReSpec: A Framework for Generating Specification using Large Language Models
Ayon, R. S., & Ahmed, S. (2026) · IEEE/ACM International Conference on AI Foundation Models and Software Engineering (FORGE) · doi:10.1145/3793655.3793731 · Cited by 6
One down, 699 to go: or, synthesising compositional desugarings
Bartha, S., Cheney, J., & Belle, V. (2021) · Proceedings of the ACM on Programming Languages · doi:10.1145/3485499 · Cited by 2
Automated Property Directed Self Composition
Shenoy, A., Prabhu, S., Madhukar, K., Shemer, R., & Srivas, M. K. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-45332-8_7 · Cited by 2
Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata
Miltner, A., Wang, Z., Chaudhuri, S., & Dillig, I. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-65633-0_3 · Cited by 2
Making Formulog Fast: An Argument for Unconventional Datalog Evaluation
Bembenek, A., Greenberg, M., & Chong, S. (2024) · Proceedings of the ACM on Programming Languages · doi:10.1145/3689754 · Cited by 2
Liou, J.-Y., Awan, M. G., Leyba, K. G., Šulc, P., Hofmeyr, S. A., Wu, C.-J., & Forrest, S. (2024) · ACM Transactions on Evolutionary Learning and Optimization · doi:10.1145/3703920 · Cited by 2
Counterexample-Guided Inference of Modular Specifications
Hallahan, W. T., Jhala, R., & Piskač, R. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3720505 · Cited by 2
Automatic Synthesis of Data-Flow Analyzers
Xu, X., Wang, X., & Xue, J. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-88806-0_22 · Cited by 2
Formal XAI via Syntax-Guided Synthesis
Bjørner, K., Judson, S., Cano, F., Goldman, D., Shoemaker, N., Piskač, R., & Könighofer, B. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-46002-9_7 · Cited by 2
LLM Based End-to-end Branch Predictor Optimization Generator
Zhai, Q., Zhang, Z., & Xiao, R. (2024) · IEEE International Conference on Application-specific Systems, Architectures and Processors (ASAP) · doi:10.1109/asap61560.2024.00050 · Cited by 2
Kim, J., Nagy, S., Reps, T., & D’Antoni, L. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3720515 · Cited by 2
ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models (CMU-CS-14-121)
Mitsch, S., & Platzer, A. (2018) · KiltHub Repository · doi:10.1184/r1/6607466 · Cited by 2
Generalizing specific-instance interpolation proofs with SyGuS
Azeem, M., Madhukar, K., & Venkatesh, R. (2018) · IEEE/ACM International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER) · doi:10.1145/3183399.3183412 · Cited by 2
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
