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 501–600 of 656
Synthesizing relation-aware entity transformation by examples
Wu, J., Jiang, Y., Xu, C., Cheung, S.-C., Ma, X., & Lu, J. J. (2018) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1145/3183440.3194963 · Cited by 2
SQL Generation from Natural Language Using Supervised Learning and Recurrent Neural Networks
Mellah, Y., Ettifouri, E. H., Rhouati, A., Dahhane, W., Bouchentouf, T., & Belkasmi, M. G. (2020) · Lecture notes in networks and systems · doi:10.1007/978-3-030-53970-2_17 · Cited by 2
Accuracy Improvement for Neural Program Synthesis via Attention Mechanism and Program Slicing
Zhang, Y., Dong, W., Wang, D., Liu, B., & Liu, J. (2020) · IEEE Annual International Computer Software and Applications Conference (COMPSAC) · doi:10.1109/compsac48688.2020.0-146 · Cited by 2
Solver-Aided Multi-Party Configuration
Kevin, D., Wagner, A., Nelson, T., Krishnamurthi, S., & Benson, T. (2020) · ACM Workshop on Hot Topics in Networks (HotNets) · doi:10.1145/3422604.3425944 · Cited by 2
Automatic parallelization of pure method calls via conditional future synthesis
Surendran, R., & Sarkar, V. (2016) · ACM SIGPLAN Notices · doi:10.1145/3022671.2984035 · Cited by 2
Deep Reinforcement Learning Guided Decision Tree Learning For Program Synthesis
Yang, M., & Zhang, D. (2023) · IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER) · doi:10.1109/saner56733.2023.00112 · Cited by 2
Pani, T., Weißenbacher, G., & Zuleger, F. (2023) · Formal Methods in System Design · doi:10.1007/s10703-023-00439-6 · Cited by 2
Synthesis of Distributed Protocols by Enumeration Modulo Isomorphisms
Egolf, D., & Tripakis, S. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-45329-8_13 · Cited by 2
Fundamental Algorithms for System Modeling, Analysis, and Optimization
Lee, E. A., Roychowdhury, J., & Seshia, S. A. (2014) · Cited by 2
Self-citationA Framework for Computer-Aided Design of Educational Domain Models
Butler, E., Torlak, E., & Popović, Z. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-73721-8_7 · Cited by 2
Self-citationConstraint Learning: An Appetizer
Teso, S. (2019) · Lecture notes in computer science · doi:10.1007/978-3-030-31423-1_7 · Cited by 2
A formal methods approach to predicting new features of the eukaryotic vesicle traffic system
Bhattacharyya, A., Gupta, A., Kuppusamy, L., Mani, S., Shukla, A., Srivas, M. K., & Thattai, M. (2019) · Acta Informatica · doi:10.1007/s00236-019-00357-3 · Cited by 2
Learning Concise Models from Long Execution Traces
Jeppu, N. Y., Melham, T., Kroening, D., & O’Leary, J. W. (2020) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1109/dac18072.2020.9218613 · Cited by 2
Solving Program Sketches with Large Integer Values
Pan, R., Hu, Q., Singh, R., & D’Antoni, L. (2020) · Lecture notes in computer science · doi:10.1007/978-3-030-44914-8_21 · Cited by 2
Self-citationBloem, R., Braud-Santoni, N., Hadžić, V., Egly, U., Lonsing, F., & Seidl, M. (2021) · Formal Methods in System Design · doi:10.1007/s10703-021-00371-7 · Cited by 2
Evolving interpretable strategies for zero-sum games
Mariño, J. R. H., & Toledo, C. F. M. (2022) · Applied Soft Computing · doi:10.1016/j.asoc.2022.108860 · Cited by 2
Osera, P.-M. (2015) · ScholarlyCommons (University of Pennsylvania) · Cited by 2
Maksimovic, D. (2015) · TSpace (University of Toronto) · Cited by 2
CVC4SY for SyGuS-COMP 2019Preprint
Reynolds, A., Barbosa, H., Nötzli, A., Barrett, C., & Tinelli, C. (2019) · arXiv (Cornell University) · doi:10.48550/arxiv.1907.10175 · Cited by 2
Few-Shot Bayesian Imitation Learning with Logical Program PoliciesPreprint
Silver, T., Allen, K. R., Lew, A. K., Kaelbling, L. P., & Tenenbaum, J. B. (2019) · arXiv (Cornell University) · doi:10.48550/arxiv.1904.06317 · Cited by 2
Automatic Synthesis of Parallel and Distributed Unix Commands with KumQuat.Preprint
Vasilakis, N., Shen, J., & Rinard, M. (2020) · arXiv (Cornell University) · Cited by 2
Kim, Y. Y., & Choi, Y. (2024) · Proceedings of the ACM on software engineering. · doi:10.1145/3643740 · Cited by 1
Buffy: A Formal Language-Based Framework for Network Performance Analysis
Seyhani, A., Zhao, J., Gupta, A., Walker, D., & Arashloo, M. T. (2024) · ACM Workshop on Hot Topics in Networks (HotNets) · doi:10.1145/3696348.3696854 · Cited by 1
The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver
Reynolds, A., Schurr, H.-J., Barbosa, H., Israel, O., Jakpor, J. Z., Lachnitt, H., Mohamed, A., Niemetz, A., Preiner, M., Zohar, Y., et al. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-32526-6_9 · Cited by 1
The Decision Problem for Regular First Order Theories
Mathur, U., Mestel, D., & Viswanathan, M. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3704870 · Cited by 1
Discovering Likely Invariants for Distributed Systems Through Runtime Monitoring and Learning
Xia, Y., Sur, D., Pingle, A., Deshmukh, J. V., Raghothaman, M., & Ravi, S. (2025) · Lecture notes in computer science · doi:10.1007/978-3-031-82700-6_1 · Cited by 1
Self-citationProgram Synthesis from Partial Traces
Ferreira, M., Nicolet, V., Dodds, J., & Kroening, D. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3729316 · Cited by 1
Weakening Goals in Logical Specifications
Andrew, B. (2025) · Lecture notes in computer science · doi:10.1007/978-3-031-94533-5_22 · Cited by 1
We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
LaFontaine, P., Zhou, Z., Mishra, A., Jagannathan, S., & Delaware, B. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3763158 · Cited by 1
Learning Event-Recording Automata Passively
Majumdar, A., Mukherjee, S., & Raskin, J.-F. (2025) · Lecture notes in computer science · doi:10.1007/978-3-032-08707-2_2 · Cited by 1
Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages
Ye, Z., Ji, R., Xiong, Y., & Zhang, X. (2026) · Proceedings of the ACM on Programming Languages · doi:10.1145/3776679 · Cited by 1
ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models
Nagy, S., Zhou, T., Polikarpova, N., & D’Antoni, L. (2026) · Proceedings of the ACM on Programming Languages · doi:10.1145/3776708 · Cited by 17
SMTgazer: Learning to Schedule SMT Algorithms via Bayesian Optimization
Luo, C. W., Cui, S., Song, J., Zhang, X., Wu, W., Liu, C., Cai, S., & Hu, C. (2025) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1109/ase63991.2025.00109 · Cited by 1
On Deductive Program Repair in Leon
Kneuss, E., Koukoutos, M., & Kunčak, V. (2015) · Infoscience (Ecole Polytechnique Fédérale de Lausanne) · Cited by 1
Secure programs via game-based synthesis
Jha, S., Reps, T., & Harris, B. (2013) · Formal Methods in Computer-Aided Design · doi:10.1109/fmcad.2013.7035519 · Cited by 1
Building an IDE for the Calculational Derivation of Imperative Programs
Chaudhari, D. L., & Damani, O. (2015) · Electronic Proceedings in Theoretical Computer Science · doi:10.4204/eptcs.187.1 · Cited by 1
MuSynth: Program Synthesis via Code Reuse and Code Manipulation
Kashyap, V., Swords, R., Schulte, E., & Melski, D. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-66299-2_8 · Cited by 1
Boosting component-based synthesis with control structure recommendation
Liu, B., Dong, W., Zhang, Y., Wang, D., & Liu, J. (2020) · doi:10.1145/3416506.3423579 · Cited by 1
Synthesizing Computable Functions from Rational Specifications Over Infinite Words
Filiot, E., & Winter, S. (2023) · International Journal of Foundations of Computer Science · doi:10.1142/s012905412348009x · Cited by 1
GPU-Accelerated Synthesis of Probabilistic Programs
Andriushchenko, R., Češka, M., Marcin, V., & Vojnar, T. (2022) · Lecture notes in computer science · doi:10.1007/978-3-031-25312-6_30 · Cited by 1
Can ChatGPT Replace a Template-based Code Generator?
Bochenek, A. (2023) · Annals of Computer Science and Information Systems · doi:10.15439/2023f5691 · Cited by 1
Saggitarius: A DSL for Specifying Grammatical Domains
Miltner, A., Loehr, D., Mong, A. C., Fisher, K. S., & Walker, D. (2023) · Proceedings of the ACM on Programming Languages · doi:10.1145/3622869 · Cited by 1
Hu, J., Chong, S., & Seltzer, M. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-71294-4_1 · Cited by 1
SemPat: From Hyperproperties to Attack Patterns for Scalable Analysis of Microarchitectural Security
Godbole, A., Manerkar, Y. A., & Seshia, S. A. (2024) · ACM SIGSAC Conference on Computer and Communications Security (CCS) · doi:10.1145/3658644.3690214 · Cited by 1
Self-citationSynthesis from multi-paradigm specifications
Filippidis, I. F., Murray, R. M., & Holzmann, G. J. (2015) · CaltechAUTHORS (California Institute of Technology) · Cited by 1
Counterexample guided inductive optimization applied to mobile robots path planning
Araújo, R. F., Ribeiro, A., de Bessa, I. V., Cordeiro, L. C., & Filho, J. E. C. (2017) · Latin American Robotics Symposium, Brazilian Symposium on Robotics and Workshop on Robotics in Education (LARS/SBR/WRE) · doi:10.1109/sbr-lars-r.2017.8215336 · Cited by 1
C Description Reconstruction Method from a Revised Netlist for ECO Support
Kimura, Y., Gharehbaghi, A. M., & Fujita, M. (2018) · IEICE Transactions on Fundamentals of Electronics Communications and Computer Sciences · doi:10.1587/transfun.e101.a.685 · Cited by 1
Synthesis of Differentiable Functional Programs for Lifelong Learning
Valkov, L., Chaudhari, D., Srivastava, A., Sutton, C. A., & Chaudhuri, S. (2018) · Cited by 1
Cross-Architecture Lifter Synthesis
van Tonder, R., & Goues, C. L. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-92970-5_10 · Cited by 1
Synthesis for Vesicle Traffic Systems
Gupta, A., Mani, S., & Shukla, A. (2018) · Lecture notes in computer science · doi:10.1007/978-3-319-99429-1_6 · Cited by 1
Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties
Ebnenasir, A. (2019) · Formal Methods in Computer-Aided Design · doi:10.23919/fmcad.2019.8894272 · Cited by 1
Programming by predicates: a formal model for interactive synthesis
Peleg, H., Itzhaky, S., Shoham, S., & Yahav, E. (2019) · Acta Informatica · doi:10.1007/s00236-019-00340-y · Cited by 1
Wang, Y., & Li, X. (2021) · IEEE Access · doi:10.1109/access.2021.3079351 · Cited by 1
Defining behaviorizeable relations to enable inference in semi-automatic program synthesis
Krasanakis, E., & Symeonidis, A. L. (2021) · Journal of Logical and Algebraic Methods in Programming · doi:10.1016/j.jlamp.2021.100714 · Cited by 1
Cavalcante, T., de Bessa, I. V., Filho, E. B. D. L., & Cordeiro, L. C. (2022) · Scientific Reports · doi:10.1038/s41598-022-19284-4 · Cited by 1
WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification
Fang, W., & Zhang, H. (2023) · Lecture notes in computer science · doi:10.1007/978-3-031-30820-8_2 · Cited by 1
Probabilistic Loop Synthesis from Sequences of Moments
Stankovič, M., & Bartocci, E. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-68416-6_14 · Cited by 1
Deductive Synthesis and Repair
Kneuss, E. (2016) · Infoscience (Ecole Polytechnique Fédérale de Lausanne) · doi:10.5075/epfl-thesis-6878 · Cited by 1
Modular Synthesis of Divide-and-Conquer Parallelism for Nested Loops (Extended Version)Preprint
Farzan, A., & Nicolet, V. (2019) · arXiv (Cornell University) · doi:10.48550/arxiv.1904.01031 · Cited by 1
Inductive Program Synthesis over Noisy Datasets using Abstraction Refinement Based OptimizationPreprint
Handa, S., & Rinard, M. (2021) · arXiv (Cornell University) · doi:10.48550/arxiv.2104.13315 · Cited by 1
Neural Guidance in Constraint Solvers
Lederman, G. (2021) · eScholarship (California Digital Library) · Cited by 1
Black-box code analysis for reverse engineering through constraint acquisition and program synthesis
Menguy, G. (2023) · theses.fr (ABES) · doi:10.70675/529006e9z5197z44eezaa10zb9838ec76479 · Cited by 1
Riener, H., Ehlers, R., & Fey, G. (2015) · Electronic Proceedings in Theoretical Computer Science · doi:10.4204/eptcs.178.3
Gauging Research in Program Synthesis with a Massive Open Online Contest
Akiba, T., Imajo, K., Iwami, H., Iwata, Y., Kataoka, T., Takahashi, N., Moskal, M., & Swamy, N. (2014)
Constraint Based Program Synthesis for Embedded Software
Eldib, H. (2015)
Approaches for Synthesis Conjectures in an SMT SolverPreprint
Reynolds, A. (2014) · arXiv (Cornell University) · doi:10.48550/arxiv.1411.3970
Superoptimizer Construction Framework with Efficient Hybrid Search
Thakur, A., Bodik, R., & Dhurjati, D. (2015)
Self-citationMethods for synthesizing predicate program pieces
Сергеевич, Ч. М., & Shelekhov, V. I. (2016) · Prikladnaya diskretnaya matematika Prilozhenie · doi:10.17223/2226308x/9/50
On ∃ ∀ ∃! solving: a case study on automated synthesis of magic card tricks
Jha, S., Raman, V., & Seshia, S. A. (2016) · Formal Methods in Computer-Aided Design · doi:10.5555/3077629.3077647
Self-citationFrehse, G., & Althoff, M. (2017) · Institute of Science and Technology Austria
Proofs as Relational Invariants of Synthesized Execution GrammarsPreprint
Voss, C., Heath, D., & Harris, W. R. (2017) · arXiv (Cornell University) · doi:10.48550/arxiv.1710.03357
Challenges for Fast Synthesis Procedures in SMT
Reynolds, A. (2018) · EPiC series in computing · doi:10.29007/xrhz
Making Automatic Theorem Provers more Versatile
Cruanes, S. (2018) · EPiC series in computing · doi:10.29007/n6j7
Constraint-Based Thread-Modular Abstract Interpretation
Kusano, M. (2018) · VTechWorks (Virginia Tech)
Contract discovery from black-box components
Sharma, V., Byun, T., McCamant, S., Rayadurgam, S., & Heimdahl, M. P. E. (2018) · doi:10.1145/3278177.3278179
Abstract Learning Frameworks for Synthesis
Löding, C., Madhusudan, P., & Neider, D. (2015) · arXiv (Cornell University) · doi:10.48550/arxiv.1507.05612
Understanding and Extending Incremental Determinization for 2QBFPreprint
Rabe, M. N., Tentrup, L., Rasmussen, C., & Seshia, S. A. (2019) · arXiv (Cornell University) · doi:10.48550/arxiv.1905.13411
Self-citationAn Overview on Formal Techniques for Understanding Digital Hardware Designs
Fey, G. (2018) · International Conference on Reliability, Infocom Technologies and Optimization (Trends and Future Directions) (ICRITO) · doi:10.1109/icrito.2018.8748750
Augmenting Neural Nets with Symbolic Synthesis: Applications to Few-Shot LearningPreprint
Murali, A., & Madhusudan, P. (2019) · arXiv (Cornell University)
Schuster, C., & Cormac Flanagan, A. (2019) · International Conference on Art, Science, and Engineering of Programming (<Programming>) · doi:10.1145/3328433.3328453
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers -- Extended VersionPreprint
Costea, A., Zhu, A., Polikarpova, N., & Sergey, I. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2001.10723
Automating Repetitive Tasks for the Masses
Gulwani, S. (2015) · ACM SIGPLAN Notices · doi:10.1145/2775051.2682621
Synthesis in Uclid5Preprint
Mora, F., Cheang, K., Polgreen, E., & Seshia, S. A. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2007.06760
Self-citationEfficient Translation of Safety LTL to DFA Using Symbolic Automata Learning and Inductive Inference
Giantamidis, G., Basagiannis, S., & Tripakis, S. (2020) · Lecture notes in computer science · doi:10.1007/978-3-030-54549-9_8
Session-layer Attack Traffic Classification by Program SynthesisPreprint
Shi, L., Li, Y., Rajeev Alur, A., & Loo, B. T. (2020) · arXiv (Cornell University) · doi:10.48550/arxiv.2010.06135
Synthesis of layout engines from relational constraints
Hottelier, T., & Bodík, R. (2015) · ACM SIGPLAN Notices · doi:10.1145/2858965.2814291
Probabilistic Synthesis for Program with Non-API Operations
Zhang, Y., Dong, W., Wang, D., Liu, J., & Liu, B. (2020) · IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C) · doi:10.1109/qrs-c51114.2020.00082
Thread-modular Counter Abstraction for Parameterized Program Safety
Pani, T., Weißenbacher, G., & Zuleger, F. (2020) · reposiTUm (TU Wien) · doi:10.34727/2020/isbn.978-3-85448-042-6_13
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank ReductionPreprint
Ish-Shalom, O., Itzhaky, S., Rinetzky, N., & Shoham, S. (2021) · arXiv (Cornell University) · doi:10.48550/arxiv.2106.00937
Automated Inference of Production Rules for Glycans
Biswas, A., Gupta, A., Missula, M., & Thattai, M. (2021) · Lecture notes in computer science · doi:10.1007/978-3-030-85633-5_4
Learning and Logic for Formal Synthesis
Caulfield, B. (2020) · eScholarship (California Digital Library)
Programming-by-example by programming-by-example: synthesis of looping programs
Berman, S. (2021) · ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) · doi:10.1145/3484271.3484977
Active Loop Detection for Applications that Access Databases
Shen, J., & Rinard, M. (2021) · DSpace@MIT (Massachusetts Institute of Technology)
Flexible Example-Based Program Synthesis on Tree-Structured Function Compositions
Mucsányi, B., Gyarmathy, B., Czapp, Á. T., & Pintér, B. (2022) · SN Computer Science · doi:10.1007/s42979-022-01090-4 · Cited by 1
On ∃ ∀ ∃! solving: A case study on automated synthesis of magic card tricks
Jha, S., Raman, V., & Seshia, S. A. (2016) · Formal Methods in Computer-Aided Design · doi:10.1109/fmcad.2016.7886664
Self-citationПетрович, Б. А. (2019) · International Workshop on Computer Science and Information Technologies (CSIT) · doi:10.2991/csit-19.2019.14
Solving Program Sketches with Large Integer Values
Hu, Q., Singh, R., & D’Antoni, L. (2022) · ACM Transactions on Programming Languages and Systems · doi:10.1145/3532849
Self-citation
Metadata
- Authors
- Alur, R., Bodik, R., Juniwal, G., Martin, M. M. K., Raghothaman, M., Seshia, S. A., Singh, R., Solar-Lezama, A., Torlak, E., & Udupa, A.
- Affiliations
- University of California, Berkeley (US)
- University of Pennsylvania (US)
- Massachusetts Institute of Technology (US)
- Venue
- 2013 Formal Methods in Computer-Aided Design
- Publisher
- IEEE
- Published
- 2013-10
- Pages
- 1-8
- OpenAlex
- W2094878426
- Cited by
- 656
- References
- 50
- Citations by year
- 2026: 29 · 2025: 45 · 2024: 48 · 2023: 55 · 2022: 49 · 2021: 65 · 2020: 64 · 2019: 63 · 2018: 61 · 2017: 58 · 2016: 54 · 2015: 37 · 2014: 25 · 2013: 3
- FWCI
- 25.24
- Type
- conference paper
- Language
- en
- Open access
- green
- hdl.handle.net
- Licence
- cc-by-nc-sa
- Locations
- Formal Methods in Computer-Aided Design (publishedVersion)
- DSpace@MIT (Massachusetts Institute of Technology) (submittedVersion, cc-by-nc-sa)
- eScholarship (California Digital Library) (submittedVersion)
- Other univ. web domain
- Funders
- National Science Foundation (1138996)
- Topics
- Physical Sciences › Computer Science › Software › Logic, programming, and type systems
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
- Keywords
- syntax-guided synthesis, program synthesis, grammar, background theory, program optimization
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
A language model drew the claims from the paper on 2026-11-05, under version 3 of the claim definition (model deepseek-v4.1-flash, prompt extract-v3).
A second model labelled each claim on 2026-11-05 (model jev-1.13-20260917, definition revision gold-guideline-v0.2).
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
