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
40 Own interpretation · 19 No basis given · 13 Own result · 12 Sources not found
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.
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
- 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
plaincorrelational- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“The exception was max3 where the stochastic solver was faster.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
plainSingle case- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“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
plainconditional- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“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:
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“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:
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
- 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plaincorrelational- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plainSingle case- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plaincorrelational- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“The current set of benchmarks is limited to synthesis of loop-free functions with no optimality criterion;”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“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
plainSingle case- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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.
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“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
hedgeddirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“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
hedged- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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.
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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.
plaincorrelational- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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:
plaincorrelational- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably 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.
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably 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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably 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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably 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.
plaincorrelational- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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:
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It 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.
hedged- Asserted: passes — The authors put it forward as true.
- Checkable: fails — It may be too vague to check against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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:
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“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:
hedged- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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:
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably 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
hedgedconditional- Asserted: passes — The authors put it forward as true.
- Checkable: fails — It may be too vague to check against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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.
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It 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
hedgedconditional- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably 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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably 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
hedgedconditional- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably 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
plainconditional- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It 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.
plaincorrelational- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plaincorrelational- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
hedgedconditional- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
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
“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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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.
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably 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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a 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
“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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
hedgedconditional- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It 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.
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
boosted- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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:
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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.
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably 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
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably 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.
Rated minor: it would not touch a result — a value no result rests on, a p-value that stays on the same side of the significance level, or a conflict that is clerical, resolved elsewhere in the paper, or outside its own findings.
In the paper
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
“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β)”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
“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 ϕ.”
Rated minor: it would not touch a result — a value no result rests on, a p-value that stays on the same side of the significance level, or a conflict that is clerical, resolved elsewhere in the paper, or outside its own findings.
In the paper
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
“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
“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
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 101–200 of 656
Strategy synthesis for linear arithmetic games
Farzan, A., & Kincaid, Z. (2017) · Proceedings of the ACM on Programming Languages · doi:10.1145/3158149 · Cited by 35
Semi-automated protocol disambiguation and code generation
Yen, J., Lévai, T., Ye, Q., Ren, X., Govindan, R., & Raghavan, B. (2021) · ACM SIGCOMM Conference (SIGCOMM) · doi:10.1145/3452296.3472910 · Cited by 39
Template-based synthesis of instruction-level abstractions for SoC verification
Subramanyan, P., Vizel, Y., Ray, S., & Malik, S. (2015) · Formal Methods in Computer-Aided Design · doi:10.1109/fmcad.2015.7542266 · Cited by 34
Combining the top-down propagation and bottom-up enumeration for inductive program synthesis
Lee, W. (2021) · Proceedings of the ACM on Programming Languages · doi:10.1145/3434335 · Cited by 34
Neurosymbolic Models for Computer Graphics
Ritchie, D., Guerrero, P., Jones, R. K., Mitra, N. J., Schulz, A., Willis, K. D. D., & Wu, J. (2023) · Computer Graphics Forum · doi:10.1111/cgf.14775 · Cited by 43
Designing Robust Software Systems through Parametric Markov Chain Synthesis
Călinescu, R., Češka, M., Gerasimou, S., Kwiatkowska, M., & Paoletti, N. (2017) · IEEE International Conference on Software Architecture (ICSA) · doi:10.1109/icsa.2017.16 · Cited by 34
Solving quantified linear arithmetic by counterexample-guided instantiation
Reynolds, A., King, T., & Kunčak, V. (2017) · Formal Methods in System Design · doi:10.1007/s10703-017-0290-y · Cited by 34
Automated lemma synthesis in symbolic-heap separation logic
Ta, Q.-T., Le, T. C., Khoo, S., & Chin, W.-N. (2017) · Proceedings of the ACM on Programming Languages · doi:10.1145/3158097 · Cited by 34
Accelerating Syntax-Guided Invariant Synthesis
Fedyukovich, G., & Bodík, R. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-89960-2_14 · Cited by 34
ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models
Mitsch, S., & Platzer, A. (2014) · Lecture notes in computer science · doi:10.1007/978-3-319-11164-3_17 · Cited by 33
Programming by Examples: Applications, Algorithms, and Ambiguity Resolution
Gulwani, S. (2016) · Lecture notes in computer science · doi:10.1007/978-3-319-40229-1_2 · Cited by 33
Kang, X., Shi, X., Wu, Y., & Ren, F. (2020) · IEEE Transactions on Affective Computing · doi:10.1109/taffc.2020.3038401 · Cited by 33
Program synthesis: challenges and opportunities
David, C., & Kroening, D. (2017) · Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences · doi:10.1098/rsta.2015.0403 · Cited by 33
Program Synthesis Using Deduction-Guided Reinforcement Learning
Chen, Y., Wang, C., Bastani, O., Dillig, I., & Feng, Y. (2020) · Lecture notes in computer science · doi:10.1007/978-3-030-53291-8_30 · Cited by 33
Bayesian synthesis of probabilistic programs for automatic data modeling
Saad, F. A., Cusumano-Towner, M., Schaechtle, U., Rinard, M., & Mansinghka, V. K. (2019) · Proceedings of the ACM on Programming Languages · doi:10.1145/3290350 · Cited by 32
Manthan: A Data-Driven Approach for Boolean Function Synthesis
Golia, P., Roy, S., & Meel, K. S. (2020) · Lecture notes in computer science · doi:10.1007/978-3-030-53291-8_31 · Cited by 32
Rahmani, K., Raza, M., Gulwani, S., Le, V., Morris, D., Radhakrishna, A., Soares, G., & Tiwari, A. (2021) · Proceedings of the ACM on Programming Languages · doi:10.1145/3485535 · Cited by 37
Adaptive Concretization for Parallel Program Synthesis
Jeon, J., Qiu, X., Solar-Lezama, A., & Foster, J. S. (2015) · Lecture notes in computer science · doi:10.1007/978-3-319-21668-3_22 · Cited by 32
Self-citationThe first reactive synthesis competition (SYNTCOMP 2014)
Jacobs, S., Bloem, R., Brenguier, R., Ehlers, R., Hell, T., Könighofer, R., Pérez, G. A., Raskin, J.-F., Ryzhyk, L., Sankur, O., et al. (2016) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-016-0416-3 · Cited by 32
Alloy*: a general-purpose higher-order relational constraint solver
Milicevic, A., Near, J. P., Kang, E., & Jackson, D. N. (2017) · Formal Methods in System Design · doi:10.1007/s10703-016-0267-2 · Cited by 32
Symbolic execution with existential second-order constraints
Mechtaev, S., Griggio, A., Cimatti, A., & Roychoudhury, A. (2018) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/3236024.3236049 · Cited by 32
Lemma Synthesis for Automating Induction over Algebraic Data Types
Yang, W., Fedyukovich, G., & Gupta, A. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-30048-7_35 · Cited by 32
Solving Quantified Bit-Vectors Using Invertibility Conditions
Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., & Tinelli, C. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-96142-2_16 · Cited by 31
Empirical Study on Synthesis Engines for Semantics-Based Program Repair
Le, X.-B. D., Lo, D., & Goues, C. L. (2016) · IEEE International Conference on Software Maintenance (ICSM) · doi:10.1109/icsme.2016.68 · Cited by 31
Optimizing homomorphic evaluation circuits by program synthesis and term rewriting
Lee, D.-K., Lee, W., Oh, H., & Yi, K. (2020) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3385412.3385996 · Cited by 30
Interactive Programming for Parametric CAD
Mathur, A. S., Pirron, M., & Damien Zufferey, A. (2020) · Computer Graphics Forum · doi:10.1111/cgf.14046 · Cited by 30
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
Nötzli, A., Reynolds, A., Barbosa, H., Niemetz, A., Preiner, M., Barrett, C., & Tinelli, C. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-24258-9_20 · Cited by 30
Few-Shot Bayesian Imitation Learning with Logical Program Policies
Silver, T., Allen, K. R., Lew, A. K., Kaelbling, L. P., & Tenenbaum, J. B. (2020) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v34i06.6587 · Cited by 30
SyGuS-Comp 2016: Results and Analysis
Rajeev Alur, A., Fisman, D., Singh, R., & Solar-Lezama, A. (2016) · Electronic Proceedings in Theoretical Computer Science · doi:10.4204/eptcs.229.13 · Cited by 29
Self-citationGeneralized data structure synthesis
Loncaric, C., Ernst, M. D., & Torlak, E. (2018) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1145/3180155.3180211 · Cited by 29
Self-citationTemplate-based circuit understanding
Gascón, A., Subramanyan, P., Dutertre, B., Tiwari, A., Jovanović, D., & Malik, S. (2014) · Formal Methods in Computer-Aided Design · doi:10.5555/2682923.2682943 · Cited by 29
Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits
Eldib, H., Wu, M., & Wang, C. (2016) · Lecture notes in computer science · doi:10.1007/978-3-319-41540-6_19 · Cited by 29
Counterexample-Guided Model Synthesis
Preiner, M., Niemetz, A., & Biere, A. (2017) · Lecture notes in computer science · doi:10.1007/978-3-662-54577-5_15 · Cited by 28
Accelerating search-based program synthesis using learned probabilistic models
Lee, W., Heo, K., Rajeev Alur, A., & Naik, M. (2018) · ACM SIGPLAN Notices · doi:10.1145/3296979.3192410 · Cited by 28
Katara: synthesizing CRDTs with verified lifting
Laddad, S., Power, C., Milano, M., Cheung, A., & Hellerstein, J. M. (2022) · Proceedings of the ACM on Programming Languages · doi:10.1145/3563336 · Cited by 28
Program Synthesis Using Dual Interpretation
Tiwari, A., Gascón, A., & Dutertre, B. (2015) · Lecture notes in computer science · doi:10.1007/978-3-319-21401-6_33 · Cited by 28
UCLID5: Integrating Modeling, Verification, Synthesis and Learning
Seshia, S. A., & Subramanyan, P. (2018) · ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE) · doi:10.1109/memcod.2018.8556946 · Cited by 28
Self-citationImitation-Projected Programmatic Reinforcement LearningPreprint
Verma, A., Le, H. M., Yue, Y., & Chaudhuri, S. (2019) · arXiv (Cornell University) · doi:10.48550/arxiv.1907.05431 · Cited by 28
Syntax-Guided Termination Analysis
Fedyukovich, G., Zhang, Y., & Gupta, A. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-96145-3_7 · Cited by 27
TF-Coder: Program Synthesis for Tensor Manipulations
Shi, K., Bieber, D., & Singh, R. (2022) · ACM Transactions on Programming Languages and Systems · doi:10.1145/3517034 · Cited by 38
Self-citationInterpretable Program Synthesis
Zhang, T., Chen, Z., Zhu, Y., Vaithilingam, P., Wang, X., & Glassman, E. L. (2021) · CHI Conference on Human Factors in Computing Systems · doi:10.1145/3411764.3445646 · Cited by 26
Automatically learning shape specifications
Zhu, H., Petri, G., & Jagannathan, S. (2016) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/2908080.2908125 · Cited by 26
Synthesis of divide and conquer parallelism for loops
Farzan, A., & Nicolet, V. (2017) · Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation · doi:10.1145/3062341.3062355 · Cited by 25
Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems
Bloem, R., Braud-Santoni, N., & Jacobs, S. (2016) · Lecture notes in computer science · doi:10.1007/978-3-319-41528-4_9 · Cited by 25
FIDEX: filtering spreadsheet data using examples
Wang, X., Gulwani, S., & Singh, R. (2016) · Conference on Object-Oriented Programming Systems, Languages, and Applications · doi:10.1145/2983990.2984030 · Cited by 25
Self-citationAutomatic Synthesis of Distributed Protocols
Rajeev Alur, A., & Tripakis, S. (2017) · ACM SIGACT News · doi:10.1145/3061640.3061652 · Cited by 25
Program Synthesis with Equivalence Reduction
Smith, C., & Albarghouthi, A. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-11245-5_2 · Cited by 25
Proving Unrealizability for Syntax-Guided Synthesis
Hu, Q., Breck, J., Cyphert, J., D’Antoni, L., & Reps, T. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-25540-4_18 · Cited by 25
Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems
Hu, Q., Cyphert, J., D'Antoni, L., & Reps, T. (2020) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3385412.3385979 · Cited by 25
Learning Probabilistic Termination Proofs
Abate, A., Giacobbe, M., & Roy, D. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-81688-9_1 · Cited by 25
L2S: A Framework for Synthesizing the Most Probable Program under a Specification
Xiong, Y., & Wang, B. (2022) · ACM Transactions on Software Engineering and Methodology · doi:10.1145/3487570 · Cited by 28
Task and Motion Policy Synthesis as Liveness Games
Wang, Y., Dantam, N. T., Chaudhuri, S., & Kavraki, L. E. (2016) · Proceedings of the International Conference on Automated Planning and Scheduling · doi:10.1609/icaps.v26i1.13792 · Cited by 24
Search-Based Local Black-Box Deobfuscation: Understand, Improve and Mitigate
Menguy, G., Bardin, S., Bonichon, R., & Lima, C. D. S. (2021) · ACM SIGSAC Conference on Computer and Communications Security (CCS) · doi:10.1145/3460120.3485250 · Cited by 24
Refutation-based synthesis in SMT
Reynolds, A., Kunčak, V., Tinelli, C., Barrett, C., & Deters, M. (2017) · Formal Methods in System Design · doi:10.1007/s10703-017-0270-2 · Cited by 24
Learning Differentially Private Mechanisms
Roy, S., Hsu, J., & Albarghouthi, A. (2021) · IEEE Symposium on Security and Privacy (S&P) · doi:10.1109/sp40001.2021.00060 · Cited by 24
Gascón, A., Tiwari, A., Carmer, B., & Mathur, U. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-63390-9 · Cited by 24
Language to Specify Syntax-Guided Synthesis ProblemsPreprint
Raghothaman, M., & Udupa, A. (2014) · arXiv (Cornell University) · doi:10.48550/arxiv.1405.5590 · Cited by 24
Self-citationTransformers in source code generation: A comprehensive survey
Ghaemi, H., Alizadehsani, Z., Shahraki, A., & Corchado, J. M. (2024) · Journal of Systems Architecture · doi:10.1016/j.sysarc.2024.103193 · Cited by 27
PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs
Andriushchenko, R., Češka, M., Junges, S., Katoen, J.-P., & Stupinský, Š. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-81685-8_40 · Cited by 23
Automatic program inversion using symbolic transducers
Hu, Q., & D’Antoni, L. (2017) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3062341.3062345 · Cited by 23
Synthesis with Abstract Examples
Drachsler-Cohen, D., Shoham, S., & Yahav, E. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-63387-9_13 · Cited by 23
Understanding and Extending Incremental Determinization for 2QBF
Rabe, M. N., Tentrup, L., Rasmussen, C., & Seshia, S. A. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-96142-2_17 · Cited by 23
Self-citationLearning Interpretable Models in the Property Specification Language
Roy, R., Fisman, D., & Neider, D. (2020) · International Joint Conference on Artificial Intelligence · doi:10.24963/ijcai.2020/306 · Cited by 23
Maximal specification synthesis
Albarghouthi, A., Dillig, I., & Gurfinkel, A. (2016) · ACM SIGPLAN Notices · doi:10.1145/2914770.2837628 · Cited by 23
Overfitting in Synthesis: Theory and Practice
Padhi, S., Millstein, T. D., Nori, A., & Sharma, R. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-25540-4_17 · Cited by 22
Guiding Enumerative Program Synthesis with Large Language Models
Li, Y., Parsert, J., & Polgreen, E. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-65630-9_15 · Cited by 32
Abstract Learning Frameworks for Synthesis
Löding, C., Madhusudan, P., & Neider, D. (2016) · Lecture notes in computer science · doi:10.1007/978-3-662-49674-9_10 · Cited by 27
Syntax-Guided Synthesis with Quantitative Syntactic Objectives
Hu, Q., & D’Antoni, L. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-96145-3_21 · Cited by 22
Inferring Inductive Invariants from Phase Structures
Feldman, Y. M. Y., Wilcox, J. R., Shoham, S., & Sagiv, M. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-25543-5_23 · Cited by 22
Beyond the elementary representations of program invariants over algebraic data types
Kostyukov, Y., Mordvinov, D., & Fedyukovich, G. (2021) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3453483.3454055 · Cited by 22
Counterexample-Driven Synthesis for Probabilistic Program Sketches
Češka, M., Hensel, C., Junges, S., & Katoen, J.-P. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-30942-8_8 · Cited by 21
Interactive synthesis of temporal specifications from examples and natural language
Gavran, I., Darulová, E., & Majumdar, R. (2020) · Proceedings of the ACM on Programming Languages · doi:10.1145/3428269 · Cited by 21
Almost correct invariants: synthesizing inductive invariants by fuzzing proofs
Lahiri, S., & Roy, S. (2022) · ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) · doi:10.1145/3533767.3534381 · Cited by 21
Polyhedral Specification and Code Generation of Sparse Tensor Contraction with Co-iteration
Zhao, T., Popoola, T., Hall, M. W., Olschanowsky, C. M., & Strout, M. M. (2022) · ACM Transactions on Architecture and Code Optimization · doi:10.1145/3566054 · Cited by 21
Counterexample-driven genetic programming
Krawiec, K., Błądek, I., & Swan, J. (2017) · Genetic and Evolutionary Computation Conference (GECCO) · doi:10.1145/3071178.3071224 · Cited by 21
Syntax-Guided Optimal Synthesis for Chemical Reaction Networks
Cardelli, L., Češka, M., Fränzle, M., Kwiatkowska, M., Laurenti, L., Paoletti, N., & Whitby, M. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-63390-9_20 · Cited by 22
Subramanyan, P., Huang, B.-Y., Vizel, Y., Gupta, A., & Malik, S. (2017) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/tcad.2017.2764482 · Cited by 21
Demystifying loops in smart contracts
Mariano, B., Chen, Y., Feng, Y., Lahiri, S. K., & Dillig, I. (2020) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/3324884.3416626 · Cited by 21
Theory Exploration Powered by Deductive Synthesis
Singher, E., & Itzhaky, S. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-81688-9_6 · Cited by 21
Optimizing synthesis with metasketches
Bornholt, J., Torlak, E., Grossman, D., & Ceze, L. (2016) · ACM SIGPLAN Notices · doi:10.1145/2914770.2837666 · Cited by 21
Self-citationComplexity verification using guided theorem enumeration
Srikanth, A., Sahin, B., & Harris, W. R. (2016) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · doi:10.1145/3009837.3009864 · Cited by 20
Data-Driven Synthesis of Provably Sound Side Channel Analyses
Wang, J., Sung, C., Raghothaman, M., & Wang, C. (2021) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse43902.2021.00079 · Cited by 20
Self-citationBoolean Abstractions for Realizability Modulo Theories
Rodríguez, A., & Sánchez, C. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-37709-9_15 · Cited by 20
HAP: SPMD DNN Training on Heterogeneous GPU Clusters with Automated Program Synthesis
Zhang, S., Diao, L., Wu, C., Cao, Z., Wang, S., & Lin, W. (2024) · European Conference on Computer Systems · doi:10.1145/3627703.3629580 · Cited by 27
Results and Analysis of SyGuS-Comp'15
Rajeev Alur, A., Fisman, D., Singh, R., & Solar-Lezama, A. (2016) · Electronic Proceedings in Theoretical Computer Science · doi:10.4204/eptcs.202.3 · Cited by 20
Self-citationTowards Bit-Width-Independent Proofs in SMT Solvers
Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C., & Tinelli, C. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-29436-6_22 · Cited by 20
Inductive program synthesis over noisy data
Handa, S., & Rinard, M. (2020) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/3368089.3409732 · Cited by 20
Program Sketching Using Lifted Analysis for Numerical Program Families
Dimovski, A. S., Apel, S., & Legay, A. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-76384-8_7 · Cited by 20
Optimal Guard Synthesis for Memory Safety
Dillig, T., Dillig, I., & Chaudhuri, S. (2014) · Lecture notes in computer science · doi:10.1007/978-3-319-08867-9_32 · Cited by 20
Applying genetic programming to PSB2: the next generation program synthesis benchmark suite
Helmuth, T., & Kelly, P. (2022) · Genetic Programming and Evolvable Machines · doi:10.1007/s10710-022-09434-y · Cited by 19
Recursion synthesis with unrealizability witnesses
Farzan, A., Lette, D., & Nicolet, V. (2022) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · doi:10.1145/3519939.3523726 · Cited by 19
Perelman, D., Gulwani, S., Grossman, D., & Provost, P. (2014) · ACM SIGPLAN Notices · doi:10.1145/2666356.2594297 · Cited by 19
Dataflow-based pruning for speeding up superoptimization
Mukherjee, M., Kant, P., Liu, Z., & Regehr, J. D. (2020) · Proceedings of the ACM on Programming Languages · doi:10.1145/3428245 · Cited by 19
Summary-based symbolic evaluation for smart contracts
Feng, Y., Torlak, E., & Bodík, R. (2020) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/3324884.3416646 · Cited by 19
Self-citationYu, Z., Liu, M., Zimmer, M., Lin, Y. C., Liu, Y., & Ren, H. M. (2025) · IEEE International Conference on LLM-Aided Design (ICLAD) · doi:10.1109/iclad65226.2025.00013 · Cited by 18
EdSketch: execution-driven sketching for Java
Hua, J., & Sarfraz Khurshid, D. (2017) · International workshop on Model Checking Software · doi:10.1145/3092282.3092285 · Cited by 18
Calibrating Research in Program Synthesis Using 72,000 Hours of Programmer Time
Akiba, T., Imajo, K., Iwami, H., Iwata, Y., Kataoka, T., Takahashi, N., Moskal, M., & Swamy, N. (2013) · Cited by 18
Data-Driven Synthesis of Full Probabilistic Programs
Chasins, S., & Phothilimthana, P. M. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-63387-9_14 · Cited by 18
Synthesizing an instruction selection rule library from semantic specifications
Buchwald, S., Fried, A., & Hack, S. (2018) · Proceedings of the CGO/Proceedings of the ... CGO · doi:10.1145/3168821 · Cited by 18
4 Regression-free Synthesis for Concurrency∗
Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., & Tarrach, T. (2014) · Cited by 18
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
