The DOI matches its Crossref record; 57 of the 57 references it cites were found in a registry or an index; none of the 14 sources its claims cite is checked for support yet.
Syntax-guided synthesis
Open accessAbstract
The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations. Our goal is to identify the core computational problem common to these proposals in a logical framework. The input to the syntax-guided synthesis problem (SyGuS) consists of a background theory, a semantic correctness specification for the desired program given by a logical formula, and a syntactic set of candidate implementations given by a grammar. The computational problem then is to find an implementation from the set of candidate expressions so that it satisfies the specification in the given theory. We describe three different instantiations of the counter-example-guided-inductive-synthesis (CEGIS) strategy for solving the synthesis problem, report on prototype implementations, and present experimental results on an initial set of benchmarks.
Overview
AI snapshot
Written from the paper’s full text.
TL;DR
This paper formalizes syntax-guided synthesis (SyGuS): given a background theory, a logical correctness specification, and a grammar of candidate expressions, find an expression satisfying the specification. It describes three CEGIS-based prototype solvers—enumerative, symbolic/constraint-based, and stochastic—and reports an initial benchmark comparison.
Key findings
- The SyGuS problem is defined as: given theory \(T\), typed function symbol \(f\), formula \(\phi\), and candidate set \(L\), find \(e \in L\) such that \(\phi[f/e]\) is valid modulo \(T\); the paper also proposes a SYNTH-LIB input format based on SMT-LIB2.
- Three CEGIS instantiations are implemented: enumerative learning, constraint-based/symbolic learning, and stochastic search; in the illustrative max example, the enumerative solver found the correct expression after only four SMT calls although about 200 expressions were enumerated and only about 80 stored.
- On 57 Hacker’s Delight benchmarks derived from 20 bit-manipulation problems, the enumerative solver dominated, followed by stochastic, while symbolic was slowest and failed to terminate on 29 of 57.
- For integer benchmarks, no solver synthesized array-search for \(n > 4\); enumerative was fastest except max3, where stochastic was faster. For parity Boolean/bit-vector benchmarks, enumerative was always faster and symbolic failed every instance; Morton benchmarks were not completed by any synthesizer.
Methods
- The paper gives a logical problem formulation with a background theory, a universally quantified first-order correctness specification, and a context-free grammar defining the candidate expression set; it also discusses encodings for multiple functions and let-expressions.
- The solving architecture is counterexample-guided inductive synthesis (CEGIS): a learning algorithm proposes a candidate from accumulated examples, and a verification oracle—implemented with an SMT solver—checks validity and returns counterexamples until a correct candidate is found or learning fails.
- The three learning strategies are: enumerative dynamic-programming search over increasing expression size with example-based pruning; symbolic component-based synthesis of loop-free programs with typing constraints and incremental SMT constraints; and stochastic Metropolis-Hastings search over parse trees with score \(\exp(-\beta C(e))\), default \(\beta=0.5\), and concurrent searches over expression sizes.
Limitations
- Stated: the current benchmark set is limited to synthesis of loop-free functions with no optimality criterion; the number of benchmarks and maturity of solvers are too limited to draw broad conclusions; prototypes were not engineered for high performance, so exact solution times are not necessarily representative.
- Stated: the symbolic solver uses a direct encoding and off-the-shelf Z3 rather than a synthesis-tuned solver, and the comparison with Sketch is “not an entirely fair comparison.”
- Evident from the text: several benchmarks timed out or could not be solved by any prototype, and the paper reports that problem encoding into grammar significantly affects performance, so the relative merits observed are preliminary.
Model-written summary. Check it against the paper before relying on it.
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
0 of 14 cited sources checked · 0 supported · 0 flagged
In the paper
“This set includes 57 different benchmarks derived from 20 different bit-manipulation problems from the book Hacker's Delight [27].”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
What the sources say
- Not matchedcites [27]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passes- Not matched
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Moreover, we observe that the enumerative technique was better than the stochastic search for all but two benchmarks,”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesA result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“We can see in the data that all solvers were affected by the encoding of the problem for at least some benchmark;”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Moreover, the enumerative solver was able to solve more hd problems than even the more optimized symbolic solver.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“This benchmark proved to be quite complex, as no solver was able to synthesize this function for n > 4.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The exception was max3 where the stochastic solver was faster.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedSingle caseTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“although in some cases, the pruning strategies used by the solvers were able to ameliorate the impact of the larger search space.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesThe paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“On the other hand, the more optimized symbolic solver did have a significant advantage in the array-search benchmarks which the enumerative solver could only solve up to size 4.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Although adding support for multiple functions does not fundamentally increase the expressiveness of the notation, it does offer significant convenience in encoding real-world synthesis problems.”
§ Syntax-Guided Synthesis > Synthesis of Multiple Functions:
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesA conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“In principle, adding support for problems with more than one unknown function is merely a matter of syntactic sugar.”
§ Syntax-Guided Synthesis > Synthesis of Multiple Functions:
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passes
- Probably not a substantial claim. 40
- It may state two separate claims as one. 31
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Thus, the mutation e = ITE(0 ≤ y, y, x) is considered with probability 1/288.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“As with other benchmarks, the enumerative solver was always faster, whereas the symbolic solver failed on every instance.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:correlational· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Aimed at formulating the core computational problem common to many recent tools for program synthesis in a canonical and logical manner, we have formalized the problem of syntax-guided synthesis.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“In the example we have described, the correct expression was examined after only four calls to the SMT solver, although about 200 expressions were enumerated by the algorithm.”
§ Syntax-Guided Synthesis > D. Enumerative Learning
Strength:plain· not yet calibratedSingle caseTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Thus, the probability of choosing e = ITE(x ≤ 0, y, x) as the initial candidate is 1/768.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“For the Hacker's Delight benchmarks (hd) we see that the enumerative solver dominates, followed by the stochastic solver.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:correlational· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“It is worth mentioning, however, that none of the grammars for these problems required the synthesizer to discover the bit-vector constants involved in the efficient implementations.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“The subexpression to mutate is chosen uniformly at random, and so the probability of deciding to mutate the boolean condition x ≤ 0 is 1/6.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Given a set of concrete examples {(-1, -4), (-1, -3), (-1, -2), (1, 1), (1, 2)}, Score(e) = exp(-2β), and Score(e ) = exp(-3β), and so e becomes the new candidate with probability exp(-β).”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The symbolic search was the slowest, failing to terminate on 29 of the 57 benchmarks.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“The current set of benchmarks is limited to synthesis of loop-free functions with no optimality criterion;”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“For instance, in the run of the algorithm on the example, although the algorithm enumerated about 200 expressions, only about 80 expressions were stored.”
§ Syntax-Guided Synthesis > D. Enumerative Learning
Strength:plain· not yet calibratedSingle caseTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Our suite includes a range of benchmarks from simple toy problems to nontrivial functions that are difficult to derive by hand.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
In the paper
“This approach provides better running times for most benchmarks in our set, but it can also be more expensive in certain cases.”
§ Syntax-Guided Synthesis > E. Constraint-based Learning
What the sources say
- Not matchedcites [5]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
- Not matched
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“With one exception, the enumerative solver is the fastest for this class of benchmarks, followed by the stochastic solver.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“The Morton benchmarks, which involve the synthesis of a function to compute Morton numbers, are intended as challenge problems, and could not be completed by any of the synthesizers.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Some of the benchmarks can be solved in a few hundredths of a second, whereas others could not be solved by any of our prototype implementations.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“If, on the other hand, e = ITE(x ≤ y, y, x) had been the mutation considered, then Score(e ) = 1, and e would have become the new candidate with probability 1.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:hedged· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“There are 768 integer-valued expressions in the grammar of size six.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✗ Based: failsProbably not a substantial claim. The paper’s conclusions may not depend on it. The paper may give no reason why it holds.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Sketch completed all but 11 of the hd benchmarks, and it was able to synthesize array-search up to size 7.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Of the 48 boolean conditions in the grammar, y ≤ 0 may be chosen with probability 1/48.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Strength:hedged· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
In the paper
“Specifically, we have transcribed all the hacker's delight and integer benchmarks into the input language of the Sketch synthesis system [24].”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
What the sources say
- Not matchedcites [24]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
- Not matched
In the paper
“Many current approaches to synthesis blend induction and deduction [22]; syntax guidance is usually a key ingredient in these approaches.”
§ Syntax-Guided Synthesis > III. INDUCTIVE SYNTHESIS Algorithmic approaches to program synthesis range over a wide spectrum, from deductive synthesis to inductive synthesis.
What the sources say
- Not matchedcites [22]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:correlational· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“In presence of let-expressions, the size directly corresponds to the number of instructions in the corresponding straight-line code, and thus such a metric can be used effectively for applications such as super-optimization.”
§ Syntax-Guided Synthesis > Optimality Criterion:
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Inductive learning is thus a natural fit for the syntax-guided synthesis problem introduced in this paper: the concept class is simply the set L of permissible expressions.”
§ Syntax-Guided Synthesis > III. INDUCTIVE SYNTHESIS Algorithmic approaches to program synthesis range over a wide spectrum, from deductive synthesis to inductive synthesis.
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Finally, it is worth noting that the statement “there exists an expression e in the language generated by a contextfree grammar G such that the formula ϕ[f /e] is valid in a theory T ” cannot be translated to determining the truth of a formula in the theory T , even with additional quantifiers.”
§ Syntax-Guided Synthesis > I. INTRODUCTION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✗ Based: failsProbably not a substantial claim. The paper’s conclusions may not depend on it. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“For example, to optimize the computation of the product of two two-by-two matrices, we can limit the search space to implementations that use only 7 multiplication operations, and such a restriction can be expressed only syntactically.”
§ Syntax-Guided Synthesis > I. INTRODUCTION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✗ Based: failsProbably not a substantial claim. The paper’s conclusions may not depend on it. The paper may give no reason why it holds. It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“First, the user can use the candidate set L to limit the search-space for potential implementations, and this has significant computational benefits for solving the synthesis problem.”
§ Syntax-Guided Synthesis > I. INTRODUCTION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
In the paper
“Many current approaches to synthesis blend induction and deduction [22]; syntax guidance is usually a key ingredient in these approaches.”
§ Syntax-Guided Synthesis > III. INDUCTIVE SYNTHESIS Algorithmic approaches to program synthesis range over a wide spectrum, from deductive synthesis to inductive synthesis.
What the sources say
- Not matchedcites [22]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:correlational· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The top-level expression specified by this grammar is the sum of two identical subexpressions built using arithmetic operators, and such a structure cannot be specified using a standard context-free grammar.”
§ Syntax-Guided Synthesis > Let Expressions in Grammar Productions:
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
None of the sources cited for this claim could be matched to a paper in Crossref, so there is nothing to check it against.
In the paper
“Counterexample-guided inductive synthesis (CEGIS) [16], [24] shown in Figure 1 is perhaps the most popular approach to inductive synthesis today.”
§ Syntax-Guided Synthesis > B. Counterexample-Guided Inductive Synthesis
What the sources say
- Not matchedcites [16]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
- Not matchedcites [24]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:hedged· not yet calibratedTests✓ Asserted: passes✗ Checkable: fails✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. It may be too vague to check against evidence. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“While let-expressions in a specification can be desugared, the same does not hold when they are used in a grammar.”
§ Syntax-Guided Synthesis > Let Expressions in Grammar Productions:
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The answer to our synthesis problem need not be unique: there may be two expressions e 1 and e 2 in the set L of allowed expressions such that both implementations satisfy the correctness specification ϕ.”
§ Syntax-Guided Synthesis > Optimality Criterion:
Load-bearingStrength:hedged· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“For example, every expression in the set L 1 is equivalent to ax+by+c, for integer constants a, b, c.”
§ Syntax-Guided Synthesis > SyGuS Problem Definition:
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Such forms of multi-modal specifications have the potential to make programming more intuitive.”
§ Syntax-Guided Synthesis > I. INTRODUCTION
Tests✓ Asserted: passes✗ Checkable: fails✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim. It may be too vague to check against evidence.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“but the overall trend we observe is that the encoding of the problem space into grammar has a significant impact on performance, although the solvers are often good at mitigating the effect of larger search spaces.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Despite these limitations, the symbolic solver was able to solve many of the benchmarks, providing a lower bound on what can be achieved with a straightforward use of off-the-shelf technology.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“This experiment is not an entirely fair comparison because, although Sketch uses a specialized constraint solver and carefully tuned encodings, the symbolic solver presented in this paper uses a direct encoding of the problem into sequences of constraints and uses Z3, a widely used offthe-shelf SMT solver which is not as aggressively tuned for synthesis problems.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Level d5, on the other extreme, involves a highly unconstrained grammar, so the synthesizer must discover which operators to use in addition to how to connect them together.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
In the paper
“Our algorithm differs from that of Schufza et al. [11] in three ways: (1) we do not attempt to optimize the size of the expression while the super-optimizer does so;”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
What the sources say
- Not matchedcites [11]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“We have some evidence to suggest that the symbolic solver can discover such constants from the full space of 2 32 possible constants with relatively little additional effort.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:hedged· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✗ Based: failsProbably not a substantial claim. The paper’s conclusions may not depend on it. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“If an answer e exists, then the search at size n = |e| is guaranteed to converge.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“We have some evidence that more optimized encodings can make the symbolic approach more competitive, although there are still many problems for which the enumerative approach is more effective.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:hedged· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“In all cases, however, the complexity of the problems derives from the size of the space of possible functions and not from the complexity of checking whether a candidate solution is correct.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✗ Based: failsProbably not a substantial claim. The paper’s conclusions may not depend on it. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“We can also see that nonsymbolic techniques can be effective in exploring spaces of implementations and can surpass symbolic techniques, especially when the problems do not require the synthesizer to derive complex bit-vector constants, which is true for all the bit-vector benchmarks used.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
None of the sources cited for this claim could be matched to a paper in Crossref, so there is nothing to check it against.
In the paper
“CEGIS has close connections to algorithmic debugging using counterexamples [19] and counterexample-guided abstraction refinement (CEGAR) [25].”
§ Syntax-Guided Synthesis > B. Counterexample-Guided Inductive Synthesis
What the sources say
- Not matchedcites [19]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
- Not matchedcites [25]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:correlational· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“However, the order of magnitude of the solution times and the relative complexity of the different approaches on different benchmarks can give us an idea of the relative merits of each of the approaches described earlier.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The problems where the enumerative solver succeeded but Sketch failed were the d5 versions of problems 11, 12, 14 and 15, which suggests that the enumerative solver was better at pruning unnecessary instructions from the grammar.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:hedged· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“For most problems, there are three different levels of grammars numbered d0, d1 and d5; level d0 involves only the instructions necessary for the implementation, so the synthesizer only needs to discover how to connect them together.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
In the paper
“The enumerative learning algorithm [8] adopts a dynamic programming based search strategy that systematically enumerates concepts (expressions) in increasing order of complexity.”
§ Syntax-Guided Synthesis > D. Enumerative Learning
What the sources say
- Not matchedcites [8]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Our prototype implementation of the three approaches to solve this problem is the first attempt to compare and contrast existing algorithms on a common set of benchmarks.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“O V can be implemented as an SMT solver that checks whether ϕ[f /e] is valid modulo the theory T .”
§ Syntax-Guided Synthesis > B. Counterexample-Guided Inductive Synthesis
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Unlike the hd benchmarks where the different grammars for a given benchmark were strict subsets of each other, in this case the encodings AIG and NAND correspond to different representations of the same space of functions.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesIt may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“None of the implementations were engineered with highperformance in mind, so the exact solution times are not necessarily representative of the best that can be achieved by a particular approach.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim. It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“so although both implementations are immature, these results suggest that it may be easier to derive good pruning rules for the explicit search than an effective fitness function for the stochastic solver.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:hedged· not yet calibratedCausal:conditional· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
In the paper
“The stochastic learning procedure is an adaptation of the algorithm recently used by Schufza et al. [11] for program super-optimization.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
What the sources say
- Not matchedcites [11]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“nevertheless, the benchmarks provide an initial demonstration of the expressiveness of the base formalism and of the relative merits of the individual solution strategies presented earlier.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:boosted· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Grammars can be conveniently used to express a wide range of constraints, and in particular, to bound the depth and/or the size of the desired expression.”
§ Syntax-Guided Synthesis > Set of Candidate Expressions:
Tests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✓ Based: passesProbably not a substantial claim. It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“On the other hand, for many of these problems the magic constants come from a handful of values such as 1, 0, or 0xffffffff, so it is unnecessary for the enumerative solver to search the space of 2 32 possible bit-vectors.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
In the paper
“(3) since we do not know the expression size n, we run concurrent searches for different values of n, whereas the super-optimizer can use the size of the input program as an upper bound on program size.”
§ Syntax-Guided Synthesis > F. Learning by Stochastic Search
What the sources say
- Not matchedcites [11]
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
Strength:plain· not yet calibratedCausal:direct· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes? Load-bearing: unclear✓ Based: passesIt may state two separate claims as one.
- Not matched
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The symbolic solver used for these experiments represents one of many possible approaches to encoding the synthesis problem into a series of constraints.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Strength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✗ Load-bearing: fails✓ Based: passesProbably not a substantial claim. The paper’s conclusions may not depend on it.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“For many problems, there are different natural ways to encode the space of desired functions into a grammar, so we are interested in observing the effect of these differences in encoding for the different solvers.”
§ Syntax-Guided Synthesis > IV. BENCHMARKS AND EVALUATION
Load-bearingStrength:plain· not yet calibratedTests✓ Asserted: passes✓ Checkable: passes✓ Load-bearing: passes✗ Based: failsProbably not a substantial claim. The paper may give no reason why it holds.
The authors state this as an assumption.
The free variables in a correctness specification are universally quantified.
“The free variables in the specification are assumed to be universally quantified: a given function f satisfies the above specification if the quantified formula ∀x, y. ϕ 1 holds, or equivalently, if the formula ϕ 1 is valid.”
The paper relies on this without support.
Existing formalization of the SMT problem and the interchange format does not provide a suitable abstraction for capturing syntactic guidance.
“Existing formalization of the SMT problem and the interchange format does not provide a suitable abstraction for capturing the syntactic guidance.”
The paper relies on this without support.
The computational engines used by the various synthesis projects rely on a small set of algorithmic ideas but have evolved independently with no mechanism for comparison, benchmarking, and sharing of back-ends.
“The computational engines used by the various synthesis projects mentioned above rely on a small set of algorithmic ideas, but have evolved independently with no mechanism for comparison, benchmarking, and sharing of back-ends.”
The paper relies on this without support.
The Metropolis-Hastings algorithm guarantees that, in the limit, expressions e are sampled with probability proportional to Score(e).
“The Metropolis-Hastings algorithm guarantees that, in the limit, expressions e are sampled with probability proportional to Score(e).”
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
The cited source doesn’t support the claim as written.
In the citing paper
“This is an approach to software development that aims to produce programs that are guaranteed to be correct with respect to their specifications from the outset, rather than relying on traditional testing and debugging methods to identify and fix errors after the fact.”
From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Alur et al., 2013
Checked by a reasoning model — may be wrong.
Experimental — accuracy not yet measuredThe check wasn’t confident either way, so it gives no verdict — never disputed.
In the citing paper
“EUSolver [Alur et al. 2017], an enumeration-based synthesizer that won the General Track of the most recent SyGuS competition [Alur et al. 2013].”
From Relational program synthesis (2018) · cites this paper as Alur et al. 2013
Experimental — accuracy not yet measured
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
Each contradiction between two passages listed here was confirmed by an independent check.
Stated scores disagree with the example evaluations
MinorUnder the stated cost definition, ITE(x ≤ 0, y, x) fails four of the five listed examples, not two. The stated mutation ITE(0 ≤ y, y, x) fails none, not three.
“Given a set of concrete examples {(-1, -4), (-1, -3), (-1, -2), (1, 1), (1, 2)}, Score(e) = exp(-2β), and Score(e ) = exp(-3β)”
“We define Score(e) to be exp(-βC(e)), where β is a smoothing constant (set by default to 0.5), and the cost function C(e) is the number of concrete examples on which e does not satisfy ϕ.”
Selected condition does not match the stated mutation
MinorThe text says the replacement condition chosen is y ≤ 0, but the resulting expression contains 0 ≤ y. Those are different conditions.
“Of the 48 boolean conditions in the grammar, y ≤ 0 may be chosen with probability 1/48.”
“Thus, the mutation e = ITE(0 ≤ y, y, x) is considered with probability 1/288.”
Citations
Cites
Quinlan, J. R. (1986) · Machine Learning · doi:10.1007/bf00116251 · Cited by 21,439
McKeown (2008) · doi:10.1145/1355734.1355746 · Cited by 8,513
Language identification in the limit
Gold, E. M. (1967) · Information and Control · doi:10.1016/s0019-9958(67)91165-5 · Cited by 3,572
Angluin, D. (1988) · Machine Learning · doi:10.1023/a:1022821128753 · Cited by 1,918
Satisfiability Modulo Theories
Barrett, C. W., Sebastiani, R., Seshia, S., et al. (2009) · Handbook of Satisfiability · doi:10.3233/978-1-58603-929-5-825 · Cited by 1,909
Self-citationGude, N. S., Koponen, T., Pettit, J., Pfaff, B., Casado, M., McKeown, N., & Shenker, S. J. (2008) · ACM SIGCOMM Computer Communication Review · doi:10.1145/1384609.1384625 · Cited by 1,447
Satisfiability Modulo Theories
Barrett, C., & Tinelli, C. (2018) · Springer eBooks · doi:10.1007/978-3-319-10575-8_11 · Cited by 1,148
Shapiro, E. Y. (1983) · doi:10.7551/mitpress/1192.001.0001 · Cited by 1,085
Counterexample-guided abstraction refinement for symbolic model checking
Clarke, E. M., Grümberg, O., Jha, S., Lu, Y., & Veith, H. (2003) · Journal of the ACM · doi:10.1145/876638.876643 · Cited by 997
(2010) · doi:10.5555/1855711.1855728 · Cited by 970
Flagged first, then by citations
Research works printed but not linked: 4
- pox, 2011, OpenFlow Controller
- shenker, 2011, The Future of Networking and the Past of Protocols"
- 0, F OpenFlow Controller
- handigol, 2009, Plug-n-Serve Load-balancing Web Traffic Using OpenFlow
Cited by
Sorted by citations
Items 601–656 of 656
Program Synthesis for Artifacts beyond Programs
Kalita, P. K. (2022) · ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) · doi:10.1145/3563768.3565544
Research on Software Synthesis Method for Spacecraft Control System
Li, Y., Dong, X., Li, X., Gu, B., Zhao, X., Qi, Y., & Yu, B. (2023) · Lecture notes in electrical engineering · doi:10.1007/978-981-19-9968-0_37
Partial bounding for recursive function synthesis
Farzan, A., & Nicolet, V. (2023) · Formal Methods in System Design · doi:10.1007/s10703-023-00417-y
AI learns to write sorting software on its own
Solar-Lezama, A. (2023) · Nature · doi:10.1038/d41586-023-01812-5
Self-citationSukhanova, A., & Sobol, V. O. (2023) · International Conference on Evaluation and Assessment in Software Engineering (EASE) · doi:10.1145/3593434.3593455
Scaling up Program Synthesis to Efficient Algorithms
Ji, R. (2023) · ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) · doi:10.1145/3618305.3623586
Sparse Format Conversion and Code Synthesis
Popoola, T. (2023) · doi:10.18122/td.2075.boisestate
Smith, D. R., & Nedunuri, S. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-60698-4_9
Model Refinement: Generating Refinements for Algorithm and System Design
Smith, D. R., & Nedunuri, S. (2024) · Lecture notes in computer science · doi:10.1007/978-3-031-66673-5_5
Two-level realization of logical formulas for deductive program synthesis
Joudakizadeh, M., & Beltiukov, A. P. (2024) · Vestnik Udmurtskogo Universiteta Matematika Mekhanika Komp yuternye Nauki · doi:10.35634/vm240401
Performance Estimation of Pattern Matching Algorithms Employing DNA Sequence
Khanna, P., Neelam, N., Manohar, Pragya, P., & Tiwari, K. (2024) · International Conference on Signal Processing and Advance Research in Computing (SPARC) · doi:10.1109/sparc61891.2024.10828785
Synthesis of Controllers for Continuous Blackbox Systems
Maderbacher, B., Windisch, F., Larrauri, A., & Bloem, R. (2025) · Lecture notes in computer science · doi:10.1007/978-3-031-82703-7_7
Metamorph: Synthesizing Large Objects from Dafny Specifications
Fedchin, A., Bai, A., & Foster, J. S. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3720448
Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction
Egolf, D., & Tripakis, S. (2025) · Lecture notes in computer science · doi:10.1007/978-3-031-90653-4_8
Towards Automatic Structured Inference of Module Abstractions
Ernst, G., & Lingsch-Rosenfeld, M. (2025) · Lecture notes in computer science · doi:10.1007/978-3-031-92196-4_15
Ebnenasir, A. (2025) · SSRN Electronic Journal · doi:10.2139/ssrn.5279961
Architecture of a System for Extracting Software Architecture from Requirements Specifications
Asenovska, N., & Stoyanova-Doycheva, A. (2025) · BRAIN BROAD RESEARCH IN ARTIFICIAL INTELLIGENCE AND NEUROSCIENCE · doi:10.70594/brain/16.2/27
Rounding meets approximate model counting
Yang, J., & Meel, K. S. (2025) · Formal Methods in System Design · doi:10.1007/s10703-025-00481-6
Godbole, A., Huffman, B. J., Liu, F., Rozas, C. V., & Seshia, S. A. (2025) · Lecture notes in computer science · doi:10.1007/978-3-031-98682-6_21
Self-citationSMT and Functional Equation Solving over the Reals: Challenges from the IMO
Brown, C. E., Chvalovský, K., Janota, M., Olšák, M., & Ratschan, S. (2025) · Lecture notes in computer science · doi:10.1007/978-3-031-99984-0_9
Program Synthesis for Geometric Modeling
Pascual, R., Gall, P. L., Belhaouari, H., & Arnould, A. (2025) · Lecture notes in computer science · doi:10.1007/978-3-032-04848-6_9
Enhancing Numerical Invariants Learning with Bounded Reachability Analysis
Bouajjani, A., Boutglay, W.-A., & Habermehl, P. (2025) · Lecture notes in computer science · doi:10.1007/978-3-032-00347-8_2
Li, M., Xiao, J., Chen, S., Ma, H., Chen, X., Bao, P., Yuan, L., & Tan, G. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3763159
Lu, S., & Bodík, R. (2025) · Proceedings of the ACM on Programming Languages · doi:10.1145/3763162
Metric-Guided Synthesis for Class Activation Mapping
Luque-Cerpa, A., Polgreen, E., Rajan, A., & Torfah, H. (2025) · Communications in computer and information science · doi:10.1007/978-3-032-08327-2_17
Identifying Potential Timing Leakages from Hardware Design with Precondition Synthesis
Chung, M., & Moon, H. (2025) · Lecture notes in computer science · doi:10.1007/978-3-032-07894-0_5
While-guard Synthesis by Abstract Static Analysis and CHC Solving
Dimovski, A. S. (2025) · Annals of Computer Science and Information Systems · doi:10.15439/2025f8874
Specification Inference Modulo Oracles for Database-Backed Web Applications
Trivedi, N. J., & Roy, S. (2025) · Lecture notes in computer science · doi:10.1007/978-981-95-3585-9_10
Quick Theory Exploration for Algebraic Data Types via Program Transformations
Ernst, G., & Fedyukovich, G. (2025) · Lecture notes in computer science · doi:10.1007/978-3-032-10794-7_21
Bottom-Up Synthesis of Memory Mutations with Separation Logic
Ferdowsi, K., & Peleg, H. (2025) · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · doi:10.4230/lipics.ecoop.2025.10
Abela, J., Cachia, E., & Layfield, C. (2025) · Mathematics · doi:10.3390/math14010041
Tensor Program Superoptimization through Cost-Guided Symbolic Program Synthesis
Brauckmann, A., Chaube, A., Magalhães, J. W. D. S., Polgreen, E., & O’boyle, M. F. P. (2026) · Proceedings of the CGO/Proceedings of the ... CGO · doi:10.1109/cgo68049.2026.11395198
Automatically Tightening Access Control Policies with Restricter
Wu, K. L., Jenkins, C., Stoller, S. D., & Chowdhury, O. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-22752-2_6 · Cited by 1
Linear temporal constraints for sketch-based synthesizers
Galicia-Mendoza, F. A., Rosenblueth, D. A., & Solar-Lezama, A. (2026) · Formal Methods in System Design · doi:10.1007/s10703-026-00495-8
Self-citationCounterexample-Guided Interval Weakening
Andrew, B., Dennis, L. A., Fisher, M., & Farrell, M. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-26752-8_1
Simplifying Mixed Boolean-Arithmetic Obfuscation by Program Synthesis and Equality Saturation
Lee, J., Lee, S. E., Cho, E.-S., & Lee, W. (2026) · ACM Transactions on Software Engineering and Methodology · doi:10.1145/3816695
Artificial Incorrectness: SMT and LLMs in Hardware Synthesis
Wang, E., Walston, J., Daniel, L., Tan, T., Zohar, Y., & Barrett, C. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-28079-4_12
Synthesizing Recursive Functional Programs via Structure-Element Separation
Lin, J., & Morihata, A. (2026) · ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE) · doi:10.1145/3814885.3816413
T4G: Trace-based P4 Program Generation
Ji, C., Jugariu, T., Dumančić, S., & Kuipers, F. A. (2026) · IEEE Conference on Computer Communications (INFOCOM) · doi:10.1109/infocom59046.2026.11571581
Active Learning of Symbolic Automata for Reactive Programs via Dynamic Symbolic Mapper
Kim, Y. Y., & Choi, Y. (2026) · Proceedings of the ACM on software engineering. · doi:10.1145/3808154
SmartIFSyn: Automated Information Flow Security Policy Synthesis for Smart Contracts
Wu, Y., Zhang, M., Song, F., & Baugh, J. W. (2026) · Proceedings of the ACM on software engineering. · doi:10.1145/3797123
Ulitzsch, V. Q., Bertani, A., Deutsch, P. W., Rodriguez, D. L., Xu, K., Gupta, A., Malik, S., & Yan, M. (2026) · IEEE Symposium on Security and Privacy (S&P) · doi:10.1109/sp63933.2026.00201
Bridging Genetic Programming and Type Theory Research
Fonseca, A. (2026) · Genetic and evolutionary computation · doi:10.1007/978-981-95-6398-2_7
Program Synthesis for Non-linear Real Arithmetic: Going Beyond Realizability
Akshay, S., Chakraborty, S., Govind, R., & Joshi, A. R. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-32589-1_15
Anvil: An Empirical Study of LLM-Powered Alloy Synthesis, Validation, and Repair
Hong, Y., Yin, C., Jiang, S., Fu, Y., & Sarfraz Khurshid, D. (2026) · ACM/IEEE International Conference on Model Driven Engineering Languages and Systems (MODELS) · doi:10.1145/3822455.3830309
Parse this! Summoning Context-Sensitive Inputs with Goblin
Lorch, R., Dar, M. D., Tinelli, C., & Chowdhury, O. (2026) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1145/3744916.3773270
A survey on fully homomorphic encryption compilers
Tian, Z., Fan, S., Deng, X., Hou, R., Meng, D., & Zhang, M. (2026) · Cybersecurity · doi:10.1186/s42400-026-00641-z
Synthesizing Graph Queries from Demonstrations
Liu, X., Liu, Q., Dyce, E., Vora, K., & Wang, Y. (2026) · Proceedings of the ACM on Programming Languages · doi:10.1145/3839524
Incremental Program Synthesis from Event Logs
Kim, J., Nicolet, V., Dodds, J., & D’Antoni, L. (2026) · Proceedings of the ACM on Programming Languages · doi:10.1145/3839460
RuSMT: An Executable Semantics as Conformance Oracle and Test Suite Synthesizer
Haghshenas, M., & Xu, M. (2026) · doi:10.1145/3842652.3843196
Smart Contract Synthesis via Multi-modal Specifications
Chen, T., Chen, H., Xiang, H., & Wang, Y. (2026) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/3832783.3837430
Margaria, T., & Steffen, B. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-40121-2
Ontology Integration as Type Inhabitation with LLM-Assisted Gap Completion
Iwamasa, M. (2026) · SICE Annual Conference (SICE) · doi:10.23919/sicefes71276.2026.11739239
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
