Pith. sign in

REVIEW 3 major objections 5 minor 27 references

Polyvariant Program Specialisation with Property-based Abstraction

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read A finite property set controls polyvariance in program specialisation, with termination and correctness preserved.

desk verdict A straightforward, honest workshop paper that unifies known instances of polyvariant CHC specialisation under a property-based abstraction; termination is sound, but the correctness claim is outsourced to external unfold-fold theorems without proof. read the letter →

arxiv 1908.07189 v1 pith:XFCII6UF submitted 2019-08-20 cs.LO cs.PL

John P. Gallagher (Roskilde University , IMDEA Software Institute) This is my paper · ORCID
classification cs.LOcs.PL MSC 68N1768Q60
keywords programspecialisationpolyvarianceconstrainedHornclausesproperty-basedabstractionpartialevaluationunfold-foldtransformationcontrol-flowrefinementterminationanalysis
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 shows that property-based abstraction—picking a finite set of properties that describe program states—can serve as a flexible, terminating control mechanism for polyvariant specialisation of constrained Horn clauses (CHCs). Polyvariant specialisation creates multiple specialised versions of the same program point under different constraints, and the paper's Algorithm 1 uses a finite property set to decide when a new version is warranted, guaranteeing that only finitely many versions are produced. The paper's examples show the same mechanism at work in loop restructuring, precondition inference, termination analysis, and proof-tree dimension decomposition, where too few properties lose information and too many add code without benefit. The author argues correctness via a closeness condition that lets the final unfold-fold step fold every input predicate to its renamed version, delegating the semantic-preservation step to general unfold-fold theorems.

What carries the argument

The generalisation operator ρΨ defined from a finite property set Ψ is the load-bearing object. For any constraint φ, ρΨ(φ) is the conjunction of every ψ ∈ Ψ entailed by φ together with every ¬ψ where φ entails ¬ψ; this is always entailed by φ, so ρΨ is a generalisation operator. Since Ψ is finite, there are only finitely many possible outputs, which bounds the number of abstract predicate versions and forces Algorithm 1's main loop to terminate. The algorithm's structure—repeatedly applying partial evaluation, collecting body atoms, abstracting them, and adding them to the working set until closure—is what connects the abstraction to the specialised program, and Lemma 1 (collect(pe(S)) ≼ S) is the property that makes the final unfold-fold transformation possible.

What would settle it

Run Algorithm 1 on a CHC program with a finite property set and compare the set of derivable answers for the entry facts in S0 before and after specialisation: any query that succeeds in one program but fails in the other, or whose answer constraint differs, would disprove the correctness claim.

Watch

Extended reading notes

Core claim

The central claim is that a finite property-based abstraction suffices to control polyvariance in a standard online specialisation algorithm without sacrificing correctness. Concretely, the algorithm starts from the entry constrained facts and repeatedly applies partial evaluation (pe), collects the atoms in the bodies of the resulting clauses, and abstracts each body atom's constraint by the generalisation operator ρΨ, which maps a constraint φ to the conjunction of all properties in Ψ entailed by φ and all negations of properties in Ψ whose negations are entailed by φ. Because Ψ is finite, ρΨ has a finite image, so the sequence of sets S grows monotonically in a finite space and reaches a fixpoint; at that fixpoint the set is closed (Lemma 1: collect(pe(S)) ≼ S), which makes it possible to fold the original clauses to their renamed versions and return a specialised program whose predicate versions are exactly the elements of S. The specialisation's granularity is therefore determined by Ψ: choosing more or fewer properties yields more or fewer specialised versions. The paper also argues, as Proposition 1, that for a fixed unfolding rule the resulting program can be minimised to an equivalent program with the fewest possible variants of each predicate, establishing a limit on how much specialisation can be achieved.

Load-bearing premise

The correctness of the final unfold-fold step is not proved in this paper; it is borrowed from general theorems about unfold-fold transformations of logic programs, and the paper only proves the closeness condition that makes the folding possible, assuming those theorems carry over to constrained Horn clauses with the chosen constraint theory.

Editorial extensions

If this is right

  • With a finite property set, the specialisation loop always terminates, so polyvariance is inherently bounded and predictable.
  • The property set is a tuning dial: choosing a subset of the program's own branch conditions can produce no specialisation at all, while richer sets generate more versions; the paper shows both extremes in Example 3.
  • For a fixed unfolding rule, the resulting specialised program can always be minimised to an equivalent program with the fewest variants (Proposition 1), so superfluous versions are harmless for the program's semantics.
  • Polyvariant specialisation acts as control-flow refinement: it can split a loop into separate loops, which makes termination and complexity analysis easier, as demonstrated on the two-loop example and in termination experiments.
  • In verification, polyvariant specialisation can expose disjunctive preconditions without needing a disjunctive analysis domain, as in the precondition-inference example.

Reading between the lines

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

  • The same algorithm could be combined with automatic property discovery: since the paper's examples choose properties from the syntactic guards in the program, a systematic method that proposes candidate properties from the constraint structure would make the approach fully automatic.
  • Because property-based abstraction is a Galois connection into a finite lattice, other finite abstract domains (e.g., intervals or predicate abstraction with boolean combinations) could be substituted for Ψ, giving a family of specialisers with different version-generation policies.
  • If the unfold-fold correctness of the final transformation is proved directly for CHCs rather than imported from logic-programming theorems, the algorithm would become a self-contained correctness result; the current paper leaves that as an appeal to prior work.
  • The automaton-minimisation view in Proposition 1 suggests a benchmark-driven test: across a suite of CHC programs, the minimal number of versions for a fixed unfolding rule should be reachable by some choice of Ψ; if not, the conjecture would need revision.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper presents Algorithm 1, an online specialisation algorithm for constrained Horn clauses (CHCs), parameterised by a generalisation operator and an unfolding rule. The core idea is to use a finite property-based abstraction, defined by a finite set of properties Psi and a generalisation operator rho_Psi, to control the polyvariance of the specialisation: the algorithm repeatedly partial-evaluates the current set of constrained facts, abstracts the collected body atoms, and adds them to the set until a closedness condition is reached; it then returns the result of an unfold-fold transformation of the collected definitions. The paper proves that rho_Psi is a generalisation operator (Lemma 2) and that the fixed-point loop yields a set S with collect(pe(S)) <= S (Lemma 1). Correctness of the final unfold-fold step is argued by reference to external unfold-fold theorems. The approach is illustrated on three applications: control-flow refinement, precondition inference, and dimension-based proof decomposition. The paper also states Proposition 1, claiming that a minimal equivalent specialisation exists and can, conjecturally, be obtained by a suitable choice of properties.

Significance. If the correctness gap is filled, the paper makes a useful conceptual contribution: it connects property-based abstraction from software model checking with polyvariant specialisation of CHCs, and shows on instructive examples how a finite property set can produce control-flow refinements and disjunctive preconditions. The algorithm is clean and the fixed-point formulation is easy to reuse. The paper is also honest about its main limitation, namely that automatic generation of the property set is left to future work. However, as it stands, the central correctness claim is delegated to unstated external results, and the optimality claim in Section 5 is only sketched; for a journal-level publication the proof foundations need to be made explicit.

major comments (3)
  1. [§3.1, Algorithm 1 line 8] The correctness of the final unfold-fold transformation is asserted but not proved. The text says correctness follows from "general results on unfold-fold transformations" [24,10,8] together with Lemma 1, but the paper neither states the resulting equivalence theorem nor checks that the hypotheses of the cited results hold for constrained Horn clauses over linear real arithmetic, for the negated constraints generated by rho_Psi, and for the particular folding using DefS. This is the load-bearing step for the advertised claim that polyvariance can be controlled "without sacrificing correctness"; the paper should either prove the equivalence theorem directly or instantiate a precise theorem from the literature and verify all side conditions.
  2. [§3, Algorithm 1 lines 4–7] The termination argument is incomplete. The statement that "the loop terminates if for some j > 0, S_{j-1}=S_j" restates the exit condition rather than proving termination. The proof obligation is to show that the ascending sequence S_j cannot grow forever; this follows from finiteness of Psi and the fact that pe(S) introduces no new predicates, but the argument should be stated as a lemma. The gap is easily fixed but is essential to the claim that Algorithm 1 is an algorithm.
  3. [§5, Proposition 1] Proposition 1 is presented as a formal result but is supported only by a proof sketch, and the stronger statement following it is explicitly labelled a conjecture. The tree-automaton minimisation argument is not defined in enough detail to be checked, the notion of equivalence "wrt derivations starting with S0" is not formalised, and the paper's conclusion that "there can be no better specialisation" in Example 3 is therefore not established. Either the proposition should be proved in full, or it should be clearly presented as a conjecture, not as a result.
minor comments (5)
  1. [§2.1] "we omit the symbol |= when clear from context" should presumably be "we omit the subscript T when clear from context".
  2. [§2.3, Definition of collect] The projection notation "phi|xi" used in the definition of collect is not defined; it should be explained (for example, as existential quantification of the remaining variables).
  3. [§3.1, Example 3] In the displayed list of definitions, "start← start, true if01..." appears to be missing a separator or line break; the formatting should be corrected for readability.
  4. [§2.1] The procedure SATT is introduced but never used in the rest of the paper; if it is only intended to justify decidability of entailment in the theory, this should be stated explicitly.
  5. [§5] The examples choose the property set Psi by hand in every case, and no heuristic or algorithm for deriving Psi from a program is presented; since the paper's practical claim depends on a reasonable choice of Psi, the discussion of automatic generation should be more than a pointer to future work.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the property set is an explicit algorithm parameter and the correctness step rests on external unfold-fold results, not on a self-citation loop.

full rationale

The paper's derivation chain is parametric rather than circular. Algorithm 1 takes the property set Psi and the unfolding rule as explicit inputs, and the dependence of the specialised program on Psi is stated openly: 'The particular choice of properties is critical for polyvariance; too few versions can result in insufficient specialisation, while too many can result in an increase of code size'. The paper also explicitly defers automatic property construction ('Further research is needed on the automatic generation of properties'), so the worked examples are illustrations of the parameter's flexibility, not independent predictions from a fitted parameter. Lemma 1 is derived directly from Definition 1 and the fixed-point structure of the loop, and the main correctness step delegates to general unfold-fold results [24,10,8], whose authors do not overlap with the present author; a missing or uninstantiated theorem is an omission, not a circular reduction. Self-citations to [18,19,9,12] are used for provenance and application context rather than to supply the central correctness theorem. I found no equation or construction in which the claimed output is definitionally equal to an input, and no self-citation chain forces the claimed result.

Assumptions & free parameters 5 free parameters · 5 assumptions · 0 invented entities

The central claim rests on several human-chosen inputs (properties, unfolding rule, a restricted generalisation in the example) and on external theorems. The paper provides no automated way to choose properties and only hand-worked examples, so the reader must accept these choices to accept the claim that property-based abstraction is a flexible control mechanism.

free parameters (5)
  • Property set Psi (Example 3)
    Manually chosen set of six constrained facts relating to control-flow tests. The polyvariance achieved depends directly on this choice.
  • Property set Psi (Example 4)
    Manually chosen properties for init, if, while to enable precondition inference; the paper notes these were generated automatically in [18] but they are inputs here.
  • Property set Psi (Example 5)
    Constraints on the dimension argument for fib and false. These are hand-picked to produce the desired dimension decomposition.
  • Unfolding rule U
    The rule used in the examples, stop at branch points or recursive predicates, is one of many possible rules; the algorithm is parameterised by U and the result depends on it.
  • Decision to apply rho only to recursive predicates
    In Example 3, generalisation is applied only to while0 facts, not to all collected facts as Algorithm 1 states; this choice affects the resulting specialisation and is not part of the stated algorithm.
assumptions (5)
  • domain assumption Satisfiability and entailment in theory T are decidable, providing SATT.
    Section 2.1 assumes a SATT procedure; all steps depend on checking phi entails psi.
  • domain assumption Unfold-fold transformation correctness results from [24, 10, 8] apply to CHCs with constraints.
    Section 3.1 correctness of line 8 relies on these external theorems.
  • domain assumption Each unfolding rule U yields a finite partial evaluation for every constrained fact.
    Definition 6 and Algorithm 1; needed for termination of the inner pe step.
  • domain assumption The CHC representation faithfully captures imperative program semantics.
    Used in examples (Figures 3, 8); standard but unproved in this paper.
  • ad hoc to paper Tree automata minimisation preserves equivalence of specialisations (Proposition 1 proof sketch).
    Proposition 1 relies on automata-theoretic minimisation; the proof is only sketched and the existence of a suitable Psi' is conjectured.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Polyvariant Program Specialisation with Property-based Abstraction." pith.science (2026). https://pith.science/paper/XFCII6UF

@misc{pith2026190807189,
  author       = {Pith},
  title        = {Pith review of: Polyvariant Program Specialisation with Property-based Abstraction},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XFCII6UF}},
  note         = {Machine review of arXiv:1908.07189}
}
read the original abstract

In this paper we show that property-based abstraction, an established technique originating in software model checking, is a flexible method of controlling polyvariance in program specialisation in a standard online specialisation algorithm. Specialisation is a program transformation that transforms a program with respect to given constraints that restrict its behaviour. Polyvariant specialisation refers to the generation of two or more specialised versions of the same program code. The same program point can be reached more than once during a computation, with different constraints applying in each case, and polyvariant specialisation allows different specialisations to be realised. A property-based abstraction uses a finite set of properties to define a finite set of abstract versions of predicates, ensuring that only a finite number of specialised versions is generated. The particular choice of properties is critical for polyvariance; too few versions can result in insufficient specialisation, while too many can result in an increase of code size with no corresponding efficiency gains. Using examples, we show the flexibility of specialisation with property-based abstraction and discuss its application in control flow refinement, verification, termination analysis and dimension-based specialisation.

Figures

Figures reproduced from arXiv: 1908.07189 by the authors.

Figure 1
Figure 1. (b) shows the result of specialising the loop with the input constraint y = 3, unfolding the loop three times and evaluating the statement y-- in the loop body. z = 1; while (y>0) { z = x*z; y--; } /* Input constraint y=3 */ z = 1; z = x*z; z = x*z; z = x*z; (a) (b) [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Polyvariant specialisation of a loop computation, once with the constraint x < 100 and the other with the constraint x ≥ 100. Polyvariant specialisation gives rise to two instances of the statement in the specialised code, s1 and s2 respectively [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 3
Figure 3. CHC representation of (a) Figure 1(a) and (b) Figure 2(a) [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: Three possible partial evaluations of constrained fact [PITH_FULL_IMAGE:figures/full_fig_p005_4.png]
Figure 5
Figure 5. Figure 5: The property to be generalised (ϕ) is shown as an area with dotted outline, and the shaded areas show the generalisation of ϕ using operation ρΨ(ϕ), where Ψ = {ψ1,ψ2,ψ3}. Example 3 Let P be the set of CHCs representing the code in [PITH_FULL_IMAGE:figures/full_fig_p00…
Figure 6
Figure 6. Figure 6: The predicate dependency graph for Example 3 [PITH_FULL_IMAGE:figures/full_fig_p008_6.png]
Figure 7
Figure 7. Figure 7: The predicate dependency graph for Example 3, with enlarged set of properties. [PITH_FULL_IMAGE:figures/full_fig_p009_7.png]
Figure 8
Figure 8. Figure 8: Example from [18]: (left) original program, (right) translation to CHCs [PITH_FULL_IMAGE:figures/full_fig_p010_8.png]
Figure 9
Figure 9. Figure 9: The predicate dependency graph for Example 4, before and after polyvariant specialisation [PITH_FULL_IMAGE:figures/full_fig_p011_9.png]
Figure 10
Figure 10. Figure 10: The dimension of a node in a tree: leaf nodes have dimension 0; a node has dimension [PITH_FULL_IMAGE:figures/full_fig_p012_10.png]
Figure 11
Figure 11. Figure 11: The predicate dependency graph for Example 5 producing clauses yielding proof trees of [PITH_FULL_IMAGE:figures/full_fig_p013_11.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

27 extracted references · 16 canonical work pages

  1. [1]

    T. Ball, A. Podelski & S. K. Rajamani (2001): Boolean and Cartesian Abstraction for Model Checking C Programs. In T. Margaria & W. Yi, editors: Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001, Proceedings , Lecture Notes in Computer Science 2031, Springer, pp. 268–283, doi:10.1007/3-540-45319-9 19

    doi:10.1007/3-540-45319-9 2001

  2. [2]

    Benkerimi & J

    K. Benkerimi & J. W. Lloyd (1990): A Partial Evaluation Procedure for Logic Programs. In S. K. Debray & M. V . Hermenegildo, editors:Logic Programming, Proceedings of the 1990 North American Conference, MIT Press, pp. 343–358

    work page 1990

  3. [3]

    Bjørner, A

    N. Bjørner, A. Gurfinkel, K. L. McMillan & A. Rybalchenko (2015): Horn Clause Solvers for Program Verification. In L. D. Beklemishev, A. Blass, N. Dershowitz, B. Finkbeiner & W. Schulte, editors: Fields of Logic and Computation II, LNCS 9300, Springer, pp. 24–51, doi:10.1007/978-3-319-23534-9 2

    doi:10.1007/978-3-319-23534-9 2015

  4. [4]

    Cousot & R

    P. Cousot & R. Cousot (1977): Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles, pp. 238–252, doi:10.1145/512950.512973

    arXiv 1977

  5. [5]

    Cousot & R

    P. Cousot & R. Cousot (1992): Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. In: 4th International Symposium on Programming Language Implementation and Logic Programming, Springer-Verlag Lecture Notes in Computer Science 631, pp. 269–295, doi:10.1007/3- 540-55844-6 142

    doi:10.1007/3- 1992

  6. [6]

    De Angelis, F

    E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2012):Specialization with Constrained Generaliza- tion for Software Model Checking. In E. Albert, editor: LOPSTR 2012, Lecture Notes in Computer Science 7844, Springer, pp. 51–70, doi:10.1007/978-3-642-38197-3 5

    work page doi:10.1007/978-3-642-38197-3 2012

  7. [7]

    De Angelis, F

    E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2014): Program verification via iterated special- ization. Sci. Comput. Program. 95, pp. 149–175, doi:10.1016/j.scico.2014.05.017

    doi:10.1016/j.scico.2014.05.017 2014

  8. [8]

    De Angelis, F

    E. De Angelis, F. Fioravanti, A. Pettorossi & M. Proietti (2018): Predicate Pairing for program verification. TPLP 18(2), pp. 126–166, doi:10.1017/S1471068417000497

    doi:10.1017/s1471068417000497 2018

Show all 27 references
  1. [9]

    Dom ´enech, S

    J. Dom ´enech, S. Genaim & J. P. Gallagher (2018): Control-Flow Refinement via Partial Evaluation . In S. Lucas, editor: 16th International Workshop on Termination (WST 2018), pp. 55–59. Available at http: //wst2018.webs.upv.es/wst2018proceedings.pdf

    2018

  2. [10]

    Etalle & M

    S. Etalle & M. Gabbrielli (1996): Transformations of CLP Modules. Theoretical Computer Science 166, pp. 101–146, doi:10.1016/0304-3975(95)00148-4. 48 Polyvariant Program Specialisation with Property-based Abstraction

    1996 doi

  3. [11]

    Fioravanti, A

    F. Fioravanti, A. Pettorossi, M. Proietti & V . Senni (2013):Controlling Polyvariance for Specialization-based Verification. Fundam. Inform. 124(4), pp. 483–502, doi:10.3233/FI-2013-845

    2013 doi

  4. [12]

    J. P. Gallagher (1993): Specialisation of Logic Programs: A Tutorial. In: Proceedings PEPM’93, ACM SIG- PLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation , ACM Press, Copen- hagen, pp. 88–98, doi:10.1145/154630.154640

    1993

  5. [14]

    J. P. Gallagher & J. C. Peralta (2001): Regular Tree Languages as an Abstract Domain in Program Speciali- sation. Higher-Order and Symbolic Computation 14(2-3), pp. 143–172, doi:10.1023/A:1012936614361

    2001 doi

  6. [15]

    Grebenshchikov, N

    S. Grebenshchikov, N. P. Lopes, C. Popeea & A. Rybalchenko (2012): Synthesizing software verifiers from proof rules. In J. Vitek, H. Lin & F. Tip, editors: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, ACM, pp. 405–416, doi:10.1145/2254064.2254112

    2012

  7. [16]

    Gulwani, S

    S. Gulwani, S. Jain & E. Koskinen (2009): Control-flow refinement and progress invariants for bound anal- ysis. In M. Hind & A. Diwan, editors: PLDI 2009, ACM, pp. 375–385, doi:10.1145/1542476.1542518

    2009

  8. [17]

    N. D. Jones, C. Gomard & P. Sestoft (1993):Partial Evaluation and Automatic Software Generation. Prentice Hall, doi:10.1016/j.scico.2004.03.010

    1993 doi

  9. [18]

    B. Kafle, J. P. Gallagher, G. Gange, P. Schachte, H. Søndergaard & P. J. Stuckey (2018): An itera- tive approach to precondition inference using constrained Horn clauses . TPLP 18(3-4), pp. 553–570, doi:10.1017/S1471068418000091

    2018 doi

  10. [19]

    B. Kafle, J. P. Gallagher & P. Ganty (2018): Tree dimension in verification of constrained Horn clauses . TPLP 18(2), pp. 224–251, doi:10.1017/S1471068418000030

    2018 doi

  11. [20]

    Leuschel & B

    M. Leuschel & B. Martens (1996): Global Control for Partial Deduction through Characteristic Atoms and Global Trees. In O. Danvy, R. Gl ¨uck & P. Thiemann, editors: Partial Evaluation, Springer-Verlag Lecture Notes in Computer Science 1110, pp. 263–283, doi:10.1007/3-540-61580-6 13

    1996 doi

  12. [21]

    Leuschel & T

    M. Leuschel & T. Massart (2000): Infinite State Model Checking by Abstract Interpretation and Program Specialisation. In A. Bossi, editor: Logic-Based Program Synthesis and Transformation (LOPSTR’99) , Springer-Verlag Lecture Notes in Computer Science1817, pp. 63–82, doi:10.100...

    2000 doi

  13. [22]

    Lloyd & J

    J. Lloyd & J. Shepherdson (1991): Partial Evaluation in Logic Programming. Journal of Logic Programming 11(3 & 4), pp. 217–242, doi:10.1016/0743-1066(91)90027-M

    1991 doi

  14. [23]

    Martens & J

    B. Martens & J. P. Gallagher (1995): Ensuring Global Termination of Partial Deduction While Allowing Flex- ible Polyvariance. In L. Sterling, editor: Proc. International Conference on Logic Programming, (ICLP’95), Tokyo, MIT Press

    1995

  15. [24]

    Pettorossi & M

    A. Pettorossi & M. Proietti (1999): Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs. J. Log. Program. 41(2-3), pp. 197–230, doi:10.1016/S0743-1066(99)00029-1

    1999 doi

  16. [25]

    Sahlin (1993): Mixtus: An Automatic Partial Avaluator for Full Prolog

    D. Sahlin (1993): Mixtus: An Automatic Partial Avaluator for Full Prolog. New Generation Comput. 12(1), pp. 7–51, doi:10.1007/BF03038271

    1993 doi

  17. [26]

    Sharma, I

    R. Sharma, I. Dillig, T. Dillig & A. Aiken (2011): Simplifying Loop Invariant Generation Using Splitter Predicates. In G. Gopalakrishnan & S. Qadeer, editors: Computer Aided Verification, CA V 2011, Lecture Notes in Computer Science 6806, Springer, pp. 703–719, doi:10.1007/978-...

    2011 doi

  18. [27]

    Turchin (1988): The Algorithm of generalization in the supercompiler

    V . Turchin (1988): The Algorithm of generalization in the supercompiler . In D. Bjørner, A. Ershov & N. Jones, editors: Proc. of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation , North- Holland, pp. 531–549

    1988

  19. [28]

    de Waal & J

    D. de Waal & J. P. Gallagher (1994): The Applicability of Logic Program Analysis and Transformation to Theorem Proving. In: Proceedings of the 12th International Conference on Automated Deduction (CADE- 12), Nancy, doi:10.1007/3-540-58156-1 15

    1994 doi

Pith tools

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