Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties

Derek Egolf; Stavros Tripakis

REVIEW 3 major objections 4 minor 21 references

Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties

T0 review · 3 major / 4 minor · reviewed 2026-08-03 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper claims a first method to synthesize recursive programs from mixed-quantifier first-order logic properties, by Skolemizing away existential quantifiers and synthesizing the resulting witness functions alongside the target program.

desk verdict Novel Skolemization-based reduction for recursive synthesis from mixed-quantifier specs; the pruning algorithm is solid, but the abstract/body benchmark mismatch must be resolved before publication. read the letter →

arxiv 2601.04045 v2 pith:NFPUHMVQ submitted 2026-01-07 cs.LO

Derek Egolf , Stavros Tripakis This is my paper · ORCID

classification cs.LO

keywords recursiveprogramsynthesismixed-quantifierspecificationsSkolemizationsketchingcounterexample-guidedsyntacticconstraintlearningprophylacticpruning

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper attempts to close a gap: existing recursive-program synthesizers accept examples or universally quantified properties, but not specifications containing both universal and existential quantifiers. It claims a reduction that turns such mixed-quantifier specifications into universal-only ones via Skolemization, adding each existential variable's witness function to the set of functions to be synthesized. The resulting synthesis problem is tackled by enumerating sketch completions, checking candidates with a counterexample generator, generalizing each counterexample into syntactic constraints on the holes, and pruning the candidate space so that invalid completions are often never constructed. The Cataclyst tool solves 41 of 42 benchmarks, and ablations indicate both counterexample generalization and prophylactic pruning substantially improve performance. The paper states its guarantee conservatively: a returned program is only known to have no counterexample found by the generator.

What carries the argument

Skolemization with synthesized witness functions: every existentially quantified variable is replaced by a fresh function symbol, and that function is synthesized together with the original target program, turning the mixed-quantifier property into a purely universal property. The second key mechanism is counterexample generalization, which records which holes were evaluated or involved in a violation and then rules out all completions that fill those holes in the same way; prophylactic pruning checks these constraints on partial completions so invalid candidates are avoided rather than merely skipped.

What would settle it

Construct a mixed-quantifier specification and a sketch whose first passing candidate is incorrect, but where the counterexample generator—using its bounded search—fails to find the violating input. If Cataclyst returns that candidate and a complete formal verification later shows the violation, the claimed correctness guarantee is falsified. More directly, one could take any known incorrect recursive program, wrap it in a sketch that exactly matches it, and check whether the tool accepts it when the counterexample generator is configured with a small search bound.

Watch

Extended reading notes

Core claim

Mixed-quantifier synthesis for recursive programs can be reduced to universal-only synthesis by treating each Skolem witness function as a first-class synthesis target: the user supplies a sketch for the witness, the tool infers its signature, and the universal solver then seeks a program-cum-witness pair satisfying the Skolemized property. The paper also shows that counterexamples can be generalized to syntactic constraints on sketch holes—such as 'hole h1 must not be (endp xs) when h2 is (tail xs)'—and that these constraints are especially powerful when checked on partial hole assignments before the rest of the sketch is filled, an approach the paper calls prophylactic pruning.

Load-bearing premise

The load-bearing premise is that when the counterexample generator returns no violation for a candidate, that candidate truly satisfies the specification; the tool stops and returns it, so if the generator misses a counterexample, the returned program can be wrong.

Editorial extensions

If this is right

Users can specify recursive functions with natural properties that contain existential quantifiers, such as 'if prefixb xs ys holds, then there exists a suffix such that ys = xs · suffix'.
The method returns a program together with a synthesized witness function, so the witness itself is executable and can be inspected or reused.
Sketches remain usable in the mixed-quantifier setting, letting users bias the search space of both the target program and the witness functions.
The approach inherits termination and contract checks: candidates must be admissible with respect to a user-supplied measure and to input contracts of background functions.
The syntactic constraints learned from counterexamples are general enough that the pruning strategy could be applied independently of the specific counterexample generator.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The same Skolem-witness synthesis idea may transfer to other synthesis settings beyond recursive programs, such as synthesizing loop invariants, relational queries, or even reactive programs from mixed-quantifier temporal specifications.
Since the learned constraints are purely syntactic and tied to hole positions, the technique could be lifted to a different backend theorem prover or SMT solver without reworking the core enumeration.
The reported gap between 41/42 benchmarks and the 42nd unsolved case suggests that prophylactic pruning's advantage grows with sketch complexity; testing on systematically larger sketches with more holes might reveal a scaling boundary.
A natural extension the paper leaves implicit is sharing counterexample constraints across multiple sketches, which could further speed up multi-function synthesis.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Quick take: the core idea is real and worth engaging: reduce mixed-quantifier recursive synthesis to ∀*-synthesis by synthesizing witness functions for Skolem symbols, then use counterexample-driven syntactic pruning. The paper explains this cleanly, and the ablations support the pruning claims. But the empirical reporting is internally inconsistent: the abstract says 60 benchmarks/59 solved and a prior tool solves 12/60, while the body says 42 benchmarks/41 solved and explicitly says prior tools are not directly comparable. That is load-bearing because the evaluation is the main evidence. It looks like a leftover from an earlier draft, but it has to be fixed.

What is genuinely new: the Skolemization reduction with user-supplied sketches for witness functions, and the prophylactic pruning that avoids enumerating partial emergents that violate learned constraints. The algorithm is clearly presented, and the generalization rules for contract, measure, and property violations are sensible. The paper is honest about the main limitation: the counterexample generator is treated as an oracle, so correctness is only 'no counterexample found.' They do post-hoc proofs for all 41 solved benchmarks, with 7 needing manual lemmas. That is reasonable, but it means the tool's guarantee is weaker than typical synthesis papers.

Soft spots besides the abstract mismatch: no formal correctness theorem for the synthesis loop itself (the enumeration and pruning are described algorithmically, but there is no proof that the algorithm returns a solution only if one exists, modulo the oracle). The tool and benchmarks are only promised, not released, so the 41/42 cannot be independently checked. And no external baseline; the 'first approach' claim is supported by the literature review, which is plausible but not independently confirmed.

For a reader, this is for the program-synthesis community, especially people working on recursive programs and property-based synthesis. I would send it to a serious referee: the idea is novel and worth the space even if the evaluation needs revision. I would not cite it in its current form until the experimental numbers are reconciled and the artifact is available.

Referee Report

3 major / 4 minor

Summary. The paper presents Cataclyst, a tool for synthesizing recursive programs from mixed-quantifier first-order logic properties. The key reduction is to Skolemize existential quantifiers and synthesize witness-generating functions for the introduced Skolem symbols alongside the target program, thereby reducing the problem to ∀*-synthesis. The ∀* loop enumerates sketch completions lazily, uses the ACL2s counterexample generator as an oracle, and learns syntactic constraints from contract, measure, and property violations to prune the candidate space, either retrospectively or prophylactically. The paper reports experimental results on a benchmark suite, with ablations showing that counterexample generalization and prophylactic pruning both improve performance.

Significance. If the claims hold, the paper makes a useful contribution: it is the first system, to my knowledge, that accepts mixed-quantifier specifications for recursive-program synthesis by synthesizing the witness functions for existential quantifiers. The algorithmic ideas — constraint learning from counterexamples and prophylactic pruning — are plausible and are evaluated in a modular way. The paper is also honest about the limitations of the counterexample generator and reports post-hoc ACL2s verification of all solved benchmarks. However, the empirical support is undercut by a major internal inconsistency between the abstract and the body, and the absence of a formal soundness/completeness statement makes the precise guarantees of the algorithm unclear.

major comments (3)

[Abstract vs. §4, §5, Tables 1–2] The abstract states a 60-benchmark suite with 59 solved and claims that a prior tool solves 12/60. The full text, however, reports a 42-benchmark suite with Proph solving 41/42, and Section 5 says that prior tools are not directly comparable and that no experimental comparison is provided. The 12/60 figure is the only quantitative comparison to prior work and appears nowhere in the body. This is a load-bearing verifiability problem: the paper's central empirical claim cannot be checked as written. The authors must reconcile the counts and either supply a reproducible external comparison or delete the 59/60 and 12/60 claims.
[§3, Fig. 2] No formal theorem states the soundness or completeness of the synthesis loop. Line 8 returns a candidate whenever cgen returns None, yet Section 4 later acknowledges that 'if it returns a program, the counterexample generator did not find a violation' and that this does not necessarily imply correctness. Likewise, line 6 says that returning None means 'no solution,' but with an incomplete cgen and unproved pruning constraints, exhaustion of the enumerated space does not establish unsatisfiability under Problem 1. The authors should either state the guarantees precisely as 'correct modulo the counterexample generator' and remove the 'no solution' phrasing, or add a theorem for the generalization and pruning steps under explicit assumptions about cgen.
[§3.2, Property Violations] The generalization step asserts that all completions sharing the same values on the 'relevant holes' exhibit the same violation. This is plausible for the examples shown, but no proof is given, and it is not obvious for properties with multiple or nested recursive calls. If the pruning constraints can overapproximate the set of incorrect programs, the algorithm may miss solutions; if they underapproximate, the performance claims are affected. A formal argument, or at least a precise characterization of when the constraint inference is sound, is needed to support the completeness and performance claims.

minor comments (4)

[§4] The statement 'Cataclyst is written in Python and will be made publicly available and submitted for artifact evaluation' is not yet verifiable. For reproducibility, include an artifact URL or release version at submission time.
[Table 1, benchmark #42] The 'ternary-tree-eq' row reports Sol. Size '—' and a timeout for all variants. Please explain why no solution size is given, e.g., because the instance is unsolved or because the size bound was not reached.
[§2.1] The running example insert property is purely universal; the mixed-quantifier features are only introduced in Section 4. This is not a flaw, but a short remark up front would help the reader map the reduction onto the examples.
[§3.2] In the contract-violation example, the phrase 'we have to satisfy the contract property ∀x,xs::(endp xs) ⇒ ¬(endp xs)' is correct only if the input contract of tail is understood as ¬(endp xs). Consider writing the contract property explicitly to avoid ambiguity.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the Skolemization reduction, candidate enumeration, and pruning are first-principles, and the benchmark-count discrepancy is a verifiability issue, not a circular derivation.

full rationale

The paper's derivation chain is self-contained and does not reduce any claimed result to its inputs. The mixed-quantifier-to-∀*-synthesis step (Section 3.5) is a genuine Skolemization reduction: existential quantifiers are eliminated by introducing new witness-generating functions, which are then synthesized alongside the target program. This is a standard and non-circular logical transformation; it does not define the target program in terms of itself, and no fitted parameter is later renamed as a prediction. The main loop (Fig. 2) enumerates candidates and checks them with the external ACL2s counterexample generator; the paper explicitly acknowledges the resulting limitation: 'if it returns a program, the counterexample generator did not find a violation of the given properties' (Section 4). That is an unsoundness/incompleteness caveat, not circularity. The pruning constraints are derived from counterexamples and are logically entailed by the observed violations, so they prune without presupposing the solution. There are no self-citations in the reference list; the cited tools (ACL2s, cgen, SyGuS solvers) are external. The experimental claims come from ablations over a fixed benchmark suite, which is a normal evaluation design. Separately, the abstract's claim of '60 benchmarks' and '12/60' for a prior tool conflicts with the full text's 42-benchmark suite and its statement that prior tools 'are not directly comparable' (Sections 4 and 5); this is an internal-consistency and reproducibility problem, but it is not a circularity and does not raise the circularity score.

Assumptions & free parameters 2 free parameters · 4 assumptions · 0 invented entities

The central claim rests on standard first-order logic and Skolemization, user-provided sketches/grammars/measures, and an external counterexample oracle whose correctness is assumed. No numeric parameters are fitted to data, and no new physical or domain entities are introduced.

free parameters (2)

Expression size bound for sketch holes = per-benchmark (solution sizes in Table 1 range from 6 to 40)
User-provided upper bound on expression size for each hole; it defines the candidate space and affects whether a solution is found. It is not fitted to a target output but is a tunable input.
Measure function per benchmark = length / number of leaves / literal input size
Termination measure is chosen by the user for each synthesis task; the paper's benchmarks use literal input size. Different choices would change which recursive candidates are admissible.

assumptions (4)

standard math Standard first-order logic validity and Skolemization are sound for eliminating existential quantifiers.
Used in Section 2.1 (e |=_B phi) and Section 3.5; the reduction assumes standard Skolemization preserves satisfiability/validity of the specification.
domain assumption The counterexample generator cgen (ACL2s) is a sound oracle: if it returns None the candidate is correct, and if it returns a counterexample the candidate is invalid.
Fig. 2 lines 7-9 accept a candidate as soon as cgen returns None; Section 4 explicitly limits the guarantee to 'did not find a violation'. This is load-bearing for soundness.
domain assumption The user provides a multi-sketch and grammar for every function under synthesis, including each introduced Skolem function.
Sections 2.3 and 3.5; without a sketch for the existential witness, the reduction cannot proceed. The grammar is also assumed to restrict variables to vars(f).
domain assumption Admissible recursive functions are those that satisfy input contracts and decrease with respect to a provided measure; termination is required for cgen to be well-defined.
Section 2.2; the synthesis problem asks for admissible implementations, so a candidate that does not terminate is rejected by cgen.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties." pith.science (2026). https://pith.science/paper/NFPUHMVQ

@misc{pith2026260104045,
  author       = {Pith},
  title        = {Pith review of: Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NFPUHMVQ}},
  note         = {Machine review of arXiv:2601.04045}
}

read the original abstract

We present a novel approach for the synthesis of recursive programs from mixed-quantifier first-order logic properties. We solve this problem using a sketching-based, enumerative, counterexample-guided approach. Our algorithm learns syntactic constraints from counterexamples to prune the candidate space and employs a prophylactic pruning technique to avoid enumerating invalid candidates altogether. We implement our technique in a tool called Cataclyst and evaluate it on a suite of 60 benchmarks. We demonstrate that both counterexample generalization and prophylactic pruning significantly improve performance. Cataclyst solves 59/60 benchmarks, while variants of Cataclyst without counterexample generalization or prophylactic pruning solve fewer benchmarks. The only other tool that can handle mixed-quantifier specifications does not support sketching, so a direct comparison is not possible. This prior tool solves 12/60 benchmarks.

Figures

Figures reproduced from arXiv: 2601.04045 by the authors.

**Figure 3.** Lazy candidate enumeration. 3.1 Lazy, On-the-fly Enumeration without Pruning A brute force algorithm can enumerate candidate programs in two phases: first enumerate all concepts from the grammar G (up to some size bound), and then combine these to obtain all possible emergents. Recall that emergents are tuples of concepts and candidate programs (sketch completions) are obtained by [PITH_FULL_IMAGE:figures/full_fig… view at source ↗

**Figure 4.** Plot comparing our tool variants using no generalization ( [PITH_FULL_IMAGE:figures/full_fig_p014_4.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

21 extracted references · 4 canonical work pages

[1]

In: Sharygina, N., Veith, H

Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8044, pp. 934–950. Springer (2013), https://doi.org/10.1007/978-3-642-39799-8_67

doi:10.1007/978-3-642-39799-8_67 2013
[2]

In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013

Alur, R., Bodík, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Se- shia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax- guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. pp. 1–8. IEEE (2013), https://ieeexplore.ieee.org/document/6679385/

arXiv 2013
[3]

In: Fisman, D., Rosu, G

Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mo- hamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial- strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems -...

2022
[4]

In: Hardin, D.S., Schmaltz, J

Chamarthi, H.R., Dillinger, P.C., Kaufmann, M., Manolios, P.: Integrating testing and interactive theorem proving. In: Hardin, D.S., Schmaltz, J. (eds.) Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011. EPTCS, vol. 70, pp. 4–19 (2011), https://doi.org/10.4204/EPTCS.70.1

work page doi:10.4204/eptcs.70.1 2011
[5]

the ACL2 sedan

Dillinger, P.C., Manolios, P., Vroon, D., Moore, J.S.: Acl2s: "the ACL2 sedan". In: 29th International Conference on Software Engineering (ICSE 2007), Minneapo- lis, MN, USA, May 20-26, 2007, Companion Volume. pp. 59–60. IEEE Computer Society (2007), https://doi.org/10.1109/ICSECOMPANION.2007.14

work page doi:10.1109/icsecompanion.2007.14 2007
[6]

CoRRabs/1510.02036(2015), http://arxiv.org/abs/1510.02036

Engelfriet, J.: Tree automata and tree grammars. CoRRabs/1510.02036(2015), http://arxiv.org/abs/1510.02036

arXiv 2015
[7]

In: Grove, D., Blackburn, S.M

Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015. pp. 229–239. ACM (2015), https://doi.org/10.1145/2737924.2737977 Recursi...

arXiv 2015
[8]

Cambridge University Press (2009)

Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)

2009

Show all 21 references

[9]

Hong, Q., Aiken, A.: Recursive program synthesis using paramorphisms. Proc. ACM Program. Lang.8(PLDI), 102–125 (2024), https://doi.org/10.1145/3656381

2024 doi
[10]

Kluwer Academic Publishers, USA (2000)

Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Ap- proach. Kluwer Academic Publishers, USA (2000)

2000
[11]

In: Hosking, A.L., Eugster, P.T., Lopes, C.V

Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive func- tions. In: Hosking, A.L., Eugster, P.T., Lopes, C.V. (eds.) Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Program- ming Systems Languages & Applications, OOPSLA 201...

2013
[12]

Lubin, J., Collins, N., Omar, C., Chugh, R.: Program sketching with live bidi- rectional evaluation. Proc. ACM Program. Lang.4(ICFP), 109:1–109:29 (2020), https://doi.org/10.1145/3408991

2020 doi
[13]

Miltner, A., Nuñez, A.T., Brendel, A., Chaudhuri, S., Dillig, I.: Bottom-up synthe- sis of recursive functional programs using angelic execution. Proc. ACM Program. Lang.6(POPL), 1–29 (2022), https://doi.org/10.1145/3498682

2022 doi
[14]

In: Gurfinkel, A., Ganesh, V

Miltner, A., Wang, Z., Chaudhuri, S., Dillig, I.: Relational synthesis of re- cursive programs via constraint annotated tree automata. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Confer- ence, CAV 2024, Montreal, QC, Canada, July 24-27...

2024 doi
[15]

In: Grove, D., Blackburn, S.M

Osera, P., Zdancewic, S.: Type-and-example-directed program synthesis. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015. pp. 619–630. ACM (2015), https://...

2015
[16]

Padhi, S., Polgreen, E., Raghothaman, M., Reynolds, A., Udupa, A.: The sygus language standard version 2.1 (2023), https://arxiv.org/abs/2312.06001

2023 arXiv
[17]

In: Krintz, C., Berger, E.D

Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. In: Krintz, C., Berger, E.D. (eds.) Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-1...

2016
[18]

In: Dillig, I., Tasiran, S

Reynolds, A., Barbosa, H., Nötzli, A., Barrett, C.W., Tinelli, C.: cvc4sy: Smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18,...

2019 doi
[19]

Solar-Lezama, A.: Program sketching. Int. J. Softw. Tools Technol. Transf.15(5-6), 475–495 (2013), https://doi.org/10.1007/s10009-012-0249-7

2013 doi
[20]

https://github.com/SyGuS-Org/benchmarks (2026), accessed: 2026-01-06

SyGuS-Org: SyGuS-Org/benchmarks: Benchmarks for SyGuS Competition (SyGuS-Comp). https://github.com/SyGuS-Org/benchmarks (2026), accessed: 2026-01-06

2026
[21]

https://github.com/cvc5/cvc5/issues/6182 (2021), gitHub issue, accessed: 2026-01-06 20 D

wonhyukchoi, ajreynol, cvc5 Contributors: Is the SyGuS keyword ‘set-feature‘ supported in CVC4? (issue #6182). https://github.com/cvc5/cvc5/issues/6182 (2021), gitHub issue, accessed: 2026-01-06 20 D. Egolf & S. Tripakis A Transposed Benchmark Table # Benchmark Holes NT sRules...

2021

Pith tools

Reviewed August 3, 2026 · model on record in the stance chip above.

[1] [1]

In: Sharygina, N., Veith, H

Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive program synthesis. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8044, pp. 934–950. Springer (2013), https://doi.org/10.1007/978-3-642-39799-8_67

doi:10.1007/978-3-642-39799-8_67 2013

[2] [2]

In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013

Alur, R., Bodík, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Se- shia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax- guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. pp. 1–8. IEEE (2013), https://ieeexplore.ieee.org/document/6679385/

arXiv 2013

[3] [3]

In: Fisman, D., Rosu, G

Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mo- hamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial- strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems -...

2022

[4] [4]

In: Hardin, D.S., Schmaltz, J

Chamarthi, H.R., Dillinger, P.C., Kaufmann, M., Manolios, P.: Integrating testing and interactive theorem proving. In: Hardin, D.S., Schmaltz, J. (eds.) Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2011, Austin, Texas, USA, November 3-4, 2011. EPTCS, vol. 70, pp. 4–19 (2011), https://doi.org/10.4204/EPTCS.70.1

work page doi:10.4204/eptcs.70.1 2011

[5] [5]

the ACL2 sedan

Dillinger, P.C., Manolios, P., Vroon, D., Moore, J.S.: Acl2s: "the ACL2 sedan". In: 29th International Conference on Software Engineering (ICSE 2007), Minneapo- lis, MN, USA, May 20-26, 2007, Companion Volume. pp. 59–60. IEEE Computer Society (2007), https://doi.org/10.1109/ICSECOMPANION.2007.14

work page doi:10.1109/icsecompanion.2007.14 2007

[6] [6]

CoRRabs/1510.02036(2015), http://arxiv.org/abs/1510.02036

Engelfriet, J.: Tree automata and tree grammars. CoRRabs/1510.02036(2015), http://arxiv.org/abs/1510.02036

arXiv 2015

[7] [7]

In: Grove, D., Blackburn, S.M

Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015. pp. 229–239. ACM (2015), https://doi.org/10.1145/2737924.2737977 Recursi...

arXiv 2015

[8] [8]

Cambridge University Press (2009)

Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)

2009