Pith. sign in

REVIEW 2 major objections 4 minor 90 references

Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis

T0 review · 2 major / 4 minor · reviewed 2026-08-11 · deepseek-v4-flash

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

Pith's one-line read This paper claims that a program is best understood as an operator, and that abstracting the operator rather than its least fixpoint yields sound and optimal abstract programs, making recurrence extraction a special case of abstract…

desk verdict Genuinely fresh semantic perspective on abstract compilation and recurrence extraction, but the 'optimal' headline is stronger than what the implementation can deliver. read the letter →

arxiv 2608.09769 v1 pith:R6OGJDRJ submitted 2026-08-10 cs.PL cs.LO

Louis Rustenholz , Alessio Mansutti , Pedro López-García , Félix Ridoux , Niki Vazou , Manuel V. Hermenegildo This is my paper · ORCID
classification cs.PLcs.LO MSC 68Q5568Q60
keywords operatorsemanticsabstractcompilationinterpretationrecurrenceextractionstaticcostanalysiscatamorphicmetricsGaloisconnectionsmonads
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 argues that least fixpoints, the standard semantic objects for recursive programs, throw away exactly the recursive structure that static cost analysis needs. It proposes operator semantics, an intermediate semantic representation in which programs are treated as operators, and performs abstraction on those operators instead of on their fixpoints. The central claim is that recurrence extraction is a special case of such operator abstraction, and that this yields optimal, solver-independent recurrences for a broad class of size metrics, called catamorphic metrics. If this is right, cost analysis becomes a matter of compiling programs into solvable recurrences through a principled sequence of abstractions.

What carries the argument

The central object is the semantic operator $\Phi = J\mathrm{Prog}K$, an endofunction on a product of Kleisli homsets that performs one simultaneous unfolding of all recursive definitions; operator semantics reifies $\Phi$ instead of passing to its least fixpoint. The key compositional primitive is Kleisli composition, and the supporting machinery includes the Kan domain/codomain abstraction (Theorem 6.8), which turns mere metric functions into Galois connections on function spaces, and abstract monads (Definition 6.14, Theorem 6.15), which abstract the effect monad itself. Catamorphic metrics, defined as functions arising from $F$-algebras via catamorphisms, are the class of metrics for which constructor and deconstructor transfer functions can be computed automatically.

What would settle it

Take a program with a catamorphic metric whose feasibility predicate the implementation overapproximates, compute both the best abstraction of the whole operator and the compositional abstract program produced by the pipeline, and exhibit an input where their least fixpoints give different upper cost bounds; that would refute the implemented optimality claim while leaving the theoretical theorems intact.

Watch

Extended reading notes

Core claim

The paper's central claim is that recurrences are abstractions of programs, made precise by abstracting the semantic operator rather than its least fixpoint. It constructs Galois connections between operator spaces: Theorem 6.12 builds an additive oplax endofunctor on a Kleisli category from mere metric functions, with no right adjoint required, and Theorem 6.15 transports an order-enriched monad through object-wise Galois connections to yield abstract monads. Together, these give optimal abstract programs that remain recursive, are often finitely representable, and whose soundness is stated by comparing operators rather than fixpoints. The framework is instantiated for recurrence-based static cost analysis over algebraic data types, supporting general function unknowns and catamorphic metrics.

Load-bearing premise

The headline optimality claim depends on exactly discarding infeasible size vectors: the abstract skip step must keep all and only those size vectors that some concrete value realises, and since that feasibility predicate is uncomputable in general, the implementation replaces it with a preliminary overapproximating analysis pass.

Editorial extensions

If this is right

  • Recurrence extraction becomes solver-independent: the same abstract operator can be analysed by postfixpoint-based solvers, symbolic manipulation, or other backends without changing the extraction step.
  • The best abstraction of an operator remains recursive, so the extracted generalised recurrence equations preserve the control-flow structure that least-fixpoint semantics discards.
  • Abstract Kleisli composition is non-associative in general, but right-associated bracketings are at least as precise as left-associated ones (Proposition 6.19), giving implementers a principled default.
  • The framework supports catamorphic metrics with conditional expressions and combinations of metrics, going beyond the metrics of established recurrence-based cost analyses.
  • Prior abstract-compilation techniques can be understood as specific implementations of the single underlying idea of optimal abstraction of operator semantics.

Reading between the lines

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

  • If the feasibility predicate used in the implementation can be made more precise, the practical gap between the proven optimality of operator abstraction and the actually extracted recurrences could close, potentially removing the main source of spurious precision loss.
  • The same operator-semantics viewpoint may transfer to probabilistic, continuous, and cyberphysical systems, since the paper's monadic machinery is not tied to the powerset effect that its cost-analysis examples use.
  • A testable extension would be to compare, on a suite of recursive programs, the recurrences produced by compositional abstract compilation against the best abstraction of the top-level operator computed outright, quantifying how much precision the compositional route loses.
  • The right-associativity result for abstract composition suggests a general design rule for higher-order abstract interpreters, and the paper leaves open whether a similar best-bracketing property holds for non-interval abstract effects such as subdistributions.
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.

Referee Report

2 major / 4 minor

Summary. The paper introduces operator semantics as a fixed-point-delaying semantic representation in which a program is identified with the monotone operator generating its recursive behaviour, rather than with its least fixpoint. It develops a categorical framework for abstracting such operators through Galois connections on operator spaces, introducing higher-order abstract domains, oplax functors, and abstract monads, with abstract composition as the central primitive. The framework is instantiated for recurrence-based static cost analysis of a small imperative language with algebraic data types: a size abstraction over catamorphic metrics yields numerical abstract programs, and an interval abstraction of the powerset monad yields systems of generalized recurrence equations. The paper proves soundness and optimality theorems for the abstract compilation constructions (Theorems 6.8, 6.12, 6.15, 6.19) and describes a prototype implementation with FOL and interval domains, explicitly deferring a detailed experimental evaluation to future work.

Significance. If the theoretical claims hold, this is a valuable unifying contribution: it makes precise the intuition that recurrence extraction is optimal abstraction of operator semantics, supports general function unknowns and catamorphic metrics, and clarifies the algebraic behaviour of abstract composition, including its non-associativity and the existence of a best bracketing. The main theorems are accompanied by detailed proofs in the text and appendices, and the framework generalizes several earlier abstract-compilation and cost-analysis approaches. The implementation section demonstrates a concrete path to the theory, but the advertised optimality is not fully realized by the implemented system. The paper is likely to appeal to a PL/static-analysis audience and to the categorical semantics community, provided the gap between the theoretical optimality claims and the implemented approximations is addressed.

major comments (2)
  1. [Section 7.1.2 / Fig. 7 (skip rule)] The implementation's best abstraction of skip is defined as the closure that removes infeasible size vectors, but the exact feasibility predicate is admitted to be non-computable in general, and the implementation overapproximates it by a preliminary analysis pass. Consequently, the extracted recurrences are sound but are not guaranteed to be the optimal abstractions claimed in the abstract and in the contribution list ('optimal recurrence extraction techniques'). The issue is structural, not an engineering detail: for a program and metric for which the overapproximation keeps a spurious size vector, the abstract operator is strictly larger than the best abstraction. The paper should either restrict the optimality claim to the ideal mathematical abstraction, identify a class of metrics/programs for which feasibility is decidable, or provide a precision bound on the overapproximation; the current wording overstates what the implementation delivers.
  2. [Sections 6.2, 6.3 and 7.1 / Fig. 7] The optimality theorems apply to the whole-operator best abstraction M(Phi) (Theorem 6.12 and Corollary 6.13), but the implemented abstract operator in Fig. 7 is built compositionally by replacing each concrete semantic clause with an abstract clause. By oplaxity, M(f ∘_T g) ≤ M(f) ∘_T M(g) can be strict, so the compositional construction is only guaranteed sound, not optimal. Footnote 12 explicitly says that 'optimal abstract compilation must avoid a too compositional approach, which can lose precision', yet the main text and contribution list present the extraction techniques as optimal without this qualification. The authors should specify exactly which artifact is optimal — the object-level best abstraction α_Φ(JProgK_Φ) or the output of the compositional pipeline — and, if the latter, give conditions under which the compositional construction coincides with the best abstraction, or weaken the claim accordingly.
minor comments (4)
  1. [Section 2, final paragraph] The bounds claimed for f_diff, f_eval, and f_diffeval are stated as provable but no proof or derivation is given; since they are used to illustrate the framework, a short appendix proof or a reference would make the example self-contained.
  2. [Section 7.2.2] The sentence 'Preliminary experiments via CAS symbolic optimisation engines suggest that computing this object directly is feasible for small-sized programs' reports no numbers or methodology; either provide the data or rephrase as an observation without quantitative claims.
  3. [Theorem 6.15 and Example 6.17] The abstract-monad construction assumes Galois insertions and representable units (γ∘α∘η = η), and the paper only shows how these assumptions are satisfied for the interval example; the limitations for other abstract effects should be stated more explicitly.
  4. [Section 8] The related-work comparison claims that the approach supports all metrics of the cited cost-analysis systems and yields more precise recurrences, but no formal statement or experimental confirmation of these comparisons is provided; this is acceptable as a positioning claim, but a brief formal argument would strengthen it.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the optimality theorems are proved in-paper; the §7.1.2 feasibility overapproximation is a computability limitation, not a circular reduction.

full rationale

The paper's derivation chain is self-contained. The central results, Theorem 6.12 and Theorem 6.15, are proved in Appendix E from definitions of Kan extensions and monad transfer; the proofs do not rely on the authors' prior works as premises. Self-citations to [79,80] occur only as examples of postfixpoint solvers and as a related prior domain-abstraction notion, not as load-bearing justifications for soundness or optimality. The one admitted limitation is in §7.1.2: 'Since the exact feasibility predicate is not computable in general, our implementation overapproximates it by a preliminary analysis of the metric definitions.' This means the implemented recurrences are sound but may be less precise than the theoretical optimum; however, this is a decidability/precision gap, not an instance where a prediction is defined by a fitted input or a theorem reduces by construction to its own assumptions. No equation equates the extracted recurrence with the abstraction parameter by definition, and no fitted value is renamed as a prediction.

Assumptions & free parameters 3 free parameters · 4 assumptions · 3 invented entities

The framework's results follow from standard order and category theory given the stated hypotheses on monads and Galois connections. The externally supplied choices are the user-provided metrics and cost model, which are not fitted to make the conclusions true. No constants are fitted to data; the claimed bounds are postfixpoints that must be checked by a solver. The ad hoc restrictions are the Galois insertion and unit-representability assumption, and the catamorphic metrics class, both flagged explicitly by the authors.

free parameters (3)
  • User-provided size metrics
    Section 7.1.1: the collection of metrics is supplied by the user via a restricted catamorphic syntax; these determine the abstract state space and the precision of the analysis. Not fitted to data.
  • Cost model = unit cost per function call, logarithmic cost for integer arithmetic
    Section 2: the cost model is chosen for the illustrative example; a modeling choice rather than a fitted parameter, but it affects the extracted cost equations.
  • Order structure and interval abstract domain
    Section 6.3 and 7.2: the choice of order-enrichment (iota) and the interval abstract monad affects precision and expressiveness; the user or analysis designer selects these. Not fitted.
assumptions (4)
  • domain assumption The monad T factors through CLat^sqcup, so all arrows T(f) are additive for the chosen order structure.
    Theorem 6.12 assumes this; it holds for powerset, W_infinity, cost monad, and counter monad used in the paper.
  • ad hoc to paper The object-wise Galois connections are Galois insertions and can represent units (gamma composed with alpha composed with eta equals eta).
    Theorem 6.15 hypothesis; for the interval example it requires injective embeddings for singletons to be representable, as stated in Example 6.17.
  • domain assumption The collection of metrics is catamorphic, meaning the size of a term depends only on the sizes of its immediate subterms.
    Section 7.1.1 restricts metrics to the catamorphic class so that transfer functions for constructors/deconstructors can be discovered automatically. Non-catamorphic metrics require user-supplied transfer functions or an overapproximation.
  • domain assumption The exact feasibility predicate is not computable, but a sound overapproximation can be computed by a preliminary analysis pass.
    Section 7.1.2 relies on this to define the implemented JskipK^sharp; this weakens the optimality guarantee from theoretical to approximate.
invented entities (3)
  • Operator semantics
    purpose: A semantic intermediate representation that treats programs as operators, preserving recursive structure while abstracting syntax.
    New semantic object introduced by the paper; internal to the framework, no external falsifiable handle.
  • Abstract monads
    purpose: Order-enriched premonads dropping associativity of Kleisli composition, so that monadic structure survives transport through Galois connections.
    Definition 6.14; internal to the framework, used to build abstract effects such as intervals.
  • Catamorphic metrics
    purpose: A class of size metrics for which abstract transfer functions can be derived automatically from the metric definitions.
    Section 7.1.1 defines the class; it is a mathematical restriction with no external evidence beyond the paper's examples.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis." pith.science (2026). https://pith.science/paper/R6OGJDRJ

@misc{pith2026260809769,
  author       = {Pith},
  title        = {Pith review of: Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/R6OGJDRJ}},
  note         = {Machine review of arXiv:2608.09769}
}
read the original abstract

Least fixpoints are fundamental to program semantics, but they abstract away the recursive structure that generated them. We introduce operator semantics: a semantic intermediate representation between syntax and classical denotational semantics, which treats programs as operators. Abstract compilation is then understood as the act of abstracting such operators. We develop higher-order abstract domains for functions, operators, and programs themselves, in which composition is the key novel primitive, together with a categorical framework for constructing sound, precise, and modular abstract compilers. We instantiate this framework in the context of recurrence-based static cost analysis, developing solver-independent, optimal recurrence extraction techniques for recursive programs over algebraic data types, that support general function unknowns and catamorphic metrics, a broad class of size metrics beyond traditional approaches.

Figures

Figures reproduced from arXiv: 2608.09769 by the authors.

Figure 1
Figure 1. Illustrative example of abstract compilation by abstraction of operator semantics. The selected operator abstraction, size abstraction, is the first step of our recurrence extraction pipeline [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Syntax of a our ImpADT language. Elements in azure allow for non-deterministic functions. projection of the tuple (𝑥1, . . . , 𝑥𝑛). The disjoint union of sets is denoted by ⊎, or simply by + when the context is clear. For a map 𝑚, element 𝑥 and value 𝑦, 𝑚[𝑥 ← 𝑦] denotes the map obtained by updating 𝑚 at 𝑥 to 𝑦, extending the domain and codomain if necessary. 4 The ImpADT language [PITH_FULL_IMAGE:figures/full_fig_p… view at source ↗
Figure 3
Figure 3. Operator semantics of the ImpADT language of [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figures from the paper (3 more)
Figure 5
Figure 5. Figure 5: Possible machine representation of domain of (operator on) interval-valued functions. Elements in [PITH_FULL_IMAGE:figures/full_fig_p024_5.png]
Figure 6
Figure 6. Figure 6: Operator semantics of the ImpADT language of [PITH_FULL_IMAGE:figures/full_fig_p038_6.png]
Figure 7
Figure 7. Figure 7: Abstract operator semantics of the ImpADT language of [PITH_FULL_IMAGE:figures/full_fig_p040_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

90 extracted references · 46 canonical work pages

  1. [1]

    Albert, P

    E. Albert, P. Arenas, S. Genaim, and G. Puebla. 2011. Closed-Form Upper Bounds in Static Cost Analysis.Journal of Automated Reasoning46, 2 (2011), 161–203. doi:10.1007/s10817-010-9174-1

    work page doi:10.1007/s10817-010-9174-1 2011

  2. [2]

    Amadio and Pierre-Louis Curien

    Roberto M. Amadio and Pierre-Louis Curien. 1998.Domains and Lambda-Calculi. Cambridge University Press, Chapter The Language PCF, 124–143. doi:10.1017/CBO9780511983504.008

    work page doi:10.1017/cbo9780511983504.008 1998

  3. [3]

    Gianluca Amato, Maria Chiara Meo, and Francesca Scozzari. 2020. On collecting semantics for program analysis. Theor. Comput. Sci.823 (2020), 1–25. doi:10.1016/J.TCS.2020.02.021

    work page doi:10.1016/j.tcs.2020.02.021 2020

  4. [4]

    Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, and Miroslav Stankovič

  5. [5]

    Davide Ancona, Andrea Corradi, Giovanni Lagorio, and Ferruccio Damiani. 2010. Abstract compilation of object- oriented languages into coinductive CLP(X): can type inference meet verification?. InProceedings of the 2010 Inter- national Conference on Formal Verification of Object-Oriented Software (FoVeOOS’10)(Paris, France). Springer-Verlag, Berlin, Heidel...

    arXiv 2010

  6. [6]

    Davide Ancona and Giovanni Lagorio. 2011. Idealized coinductive type systems for imperative object-oriented programs.RAIRO - Theoretical Informatics and Applications45, 1 (Jan. 2011), 3–33. doi:10.1051/ita/2011009

    arXiv 2011

  7. [7]

    Davide Ancona and Giovanni Lagorio. 2012. Static Single Information Form for Abstract Compilation.Theoretical Computer Science(2012), 10–27. doi:10.1007/978-3-642-33475-7_2

    work page doi:10.1007/978-3-642-33475-7_2 2012

  8. [8]

    Dominique Boucher and Marc Feeley. 1996. Abstract compilation: A new implementation paradigm for static analysis. In Compiler Construction (CC), Tibor Gyimóthy (Ed.). Springer Berlin Heidelberg, 192–207. doi:10.1007/3-540-61053-7_62

    work page doi:10.1007/3-540-61053-7_62 1996

Show all 90 references
  1. [9]

    François Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings. InFormal Methods in Programming and Their Applications, Dines Bjørner, Manfred Broy, and Igor V. Pottosin (Eds.). Springer Berlin Heidelberg, Berlin, Abstract Compilation as Abstraction of Operat...

    1993 doi

  2. [10]

    Ajay Brahmakshatriya, Saman Amarasinghe, and Martin Rinard. 2026. Backwards Data-Flow Analysis using Prophecy Variables in the BuildIt System. arXiv:2601.02653 [cs.PL] https://arxiv.org/abs/2601.02653

    2026

  3. [11]

    Jason Breck, John Cyphert, Zachary Kincaid, and Thomas W. Reps. 2020. Templates and recurrences: better together. InPLDI. ACM, 688–702. doi:10.1145/3385412.3386035

    2020

  4. [12]

    Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and Jürgen Giesl. 2014. Alternating runtime and size complexity analysis of integer programs. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 140–15...

    2014 doi

  5. [13]

    Marc Chevalier and Jérôme Feret. 2020. Sharing Ghost Variables in a Collection of Abstract Domains. InVerification, Model Checking, and Abstract Interpretation (VMCAI), Dirk Beyer and Damien Zufferey (Eds.). Springer International Publishing, Cham, 158–179. doi:10.1007/978-3-0...

    2020 doi

  6. [14]

    2021.Principles of Abstract Interpretation

    Patrick Cousot. 2021.Principles of Abstract Interpretation. MIT Press. ISBN: 9780262044905

    2021

  7. [15]

    Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. InACM Symposium on Principles of Programming Languages (POPL’77). ACM Press, 238–252. doi:10.1145/512950.512973

    1977

  8. [16]

    Patrick Cousot and Radhia Cousot. 1979. Systematic Design of Program Analysis Frameworks. InSixth ACM Symposium on Principles of Programming Languages (POPL). San Antonio, Texas, 269–282. doi:10.1145/567752.567778

    1979

  9. [17]

    Patrick Cousot and Radhia Cousot. 2002. Systematic Design of Program Transformation Frameworks by Abstract Interpretation. InPOPL’02: 29ST ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, Portland, Oregon, 178–190. doi:10.1145/503272.503290

    2002

  10. [18]

    Patrick Cousot and Radhia Cousot. 2014. A galois connection calculus for abstract interpretation. InPOPL. ACM, 3–4. doi:10.1145/2535838.2537850

    2014

  11. [19]

    John Cyphert and Zachary Kincaid. 2024. Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis.Proc. ACM Program. Lang.8, POPL, Article 25 (Jan. 2024), 29 pages. doi:10.1145/3632867

    2024 doi

  12. [20]

    Gallagher, Manuel V

    Emanuele De Angelis, Fabio Fioravanti, John P. Gallagher, Manuel V. Hermenegildo, Alberto Pettorossi, and Maurizio Proietti. 2021. Analysis and Transformation of Constrained Horn Clauses for Program Verification.TPLP22, 6 (2021), 1–69. doi:10.1017/S1471068421000211

    2021 doi

  13. [21]

    Emanuele de Angelis, Fabio Fioravanti, Alberto Pettorossi, and Maurizio Proietti. 2024. Catamorphic Abstractions for Constrained Horn Clause Satisfiability.Theory and Practice of Logic Programming25, 1 (Oct. 2024), 64–91. doi:10.1017/s147106842400019x

    2024 doi

  14. [22]

    Emanuele de Angelis, Maurizio Proietti, Fabio Fioravanti, and Alberto Pettorossi. 2022. Verifying Catamorphism- Based Contracts using Constrained Horn Clauses.Theory and Practice of Logic Programming22, 4 (2022), 555–572. doi:10.1017/S1471068422000175

    2022 doi

  15. [23]

    S. K. Debray and N.-W. Lin. 1993. Cost Analysis of Logic Programs.ACM TOPLAS15, 5 (November 1993), 826–875. doi:10.1145/161468.161472

    1993

  16. [24]

    S. K. Debray, N.-W. Lin, and M.V. Hermenegildo. 1990. Task Granularity Analysis in Logic Programs. InProc. PLDI’90. ACM, 174–188. doi:10.1145/93542.93564

    1990

  17. [25]

    S. K. Debray, P. Lopez-Garcia, M.V. Hermenegildo, and N.-W. Lin. 1997. Lower Bound Cost Estimation for Logic Programs. InILPS’97. MIT Press, 291–305. doi:10.7551/mitpress/4283.003.0035

    1997 doi

  18. [26]

    S. K. Debray and D. S. Warren. 1988. Automatic Mode Inference for Logic Programs.Journal of Logic Programming (5) (1988), 207–229. doi:10.1016/0743-1066(88)90010-6

    1988 doi

  19. [27]

    Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. 2017. Efficient Coalgebraic Partition Refinement. In28th International Conference on Concurrency Theory (CONCUR 2017) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 85), Roland Meyer and Uwe N...

    2017 doi

  20. [28]

    Azadeh Farzan and Zachary Kincaid. 2015. Compositional Recurrence Analysis. InFormal Methods in Computer-Aided Design, FMCAD. IEEE, 57–64. doi:10.1109/FMCAD.2015.7542253

    2015

  21. [29]

    Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. 2014. The Spirit of Ghost Code. InComputer Aided Verification (CA V). doi:10.1007/978-3-319-08867-9_1

    2014 doi

  22. [30]

    2017.Cost Analysis of Programs Based on the Refinement of Cost Relations

    Antonio Flores-Montoya. 2017.Cost Analysis of Programs Based on the Refinement of Cost Relations. Ph. D. Dissertation. T.U. Darmstadt. doi:10.26083/tuprints-00006746 Advisor: Reiner Hähnle

    2017 doi

  23. [31]

    Nate Foster, Dexter Kozen, Mae Milano, Alexandra Silva, and Laure Thompson. 2015. A Coalgebraic Decision Procedure for NetKAT.Proc. ACM Program. Lang.50, POPL (2015), 50:343–50:355. doi:10.1145/2775051.2677011

    2015

  24. [32]

    Gallagher

    J.P. Gallagher. 1993. Tutorial on Specialisation of Logic Programs. InProceedings of PEPM’93, the ACM Sigplan Symposium on Partial Evaluation and Semantics-Based Program Manipulation. ACM Press, 88–98. doi:10.1145/154630. 154640 28 Louis Rustenholz et al

    1993 doi

  25. [33]

    Roberto Giacobazzi and Francesco Ranzato. 1999. The reduced relative power operation on abstract domains.Theoretical Computer Science216, 1 (1999), 159–211. doi:10.1016/S0304-3975(98)00194-7

    1999 doi

  26. [34]

    Goharshady, S

    Amir K. Goharshady, S. Hitarth, and Sergei Novozhilov. 2025. Efficient Synthesis of Tight Polynomial Upper-Bounds for Systems of Conditional Polynomial Recurrences. InESOP 2025. doi:10.1007/978-3-031-91121-7_1

    2025 doi

  27. [35]

    Sergey Goncharov and Lutz Schröder. 2013. A Relatively Complete Generic Hoare Logic for Order-Enriched Effects. In 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013). 273–282. doi:10.1109/LICS.2013.33

    2013 doi

  28. [36]

    Ichiro Hasuo. 2015. Generic weakest precondition semantics from monads enriched with order.Theoretical Computer Science604 (2015), 2–29. doi:10.1016/j.tcs.2015.03.047 Special Issue on Coalgebraic Methods in Computer Science (CMCS’14)

    2015 doi

  29. [37]

    Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. 2007. Generic Trace Semantics via Coinduction.Logical Methods in Computer ScienceVolume 3, Issue 4, Article 11 (Nov 2007). doi:10.2168/LMCS-3(4:11)2007

    2007 doi

  30. [38]

    Ichiro Hasuo and Kohei Suenaga. 2012. Exercises in Nonstandard Static Analysis of Hybrid Systems. InCA V. doi:10. 1007/978-3-642-31424-7_34

    2012

  31. [39]

    Hermenegildo, G

    M.V. Hermenegildo, G. Puebla, F. Bueno, and P. Lopez-Garcia. 2005. Integrated Program Debugging, Verification, and Optimization Using Abstract Interpretation (and The Ciao System Preprocessor).Science of Comp. Progr.58, 1–2 (2005)

    2005

  32. [40]

    Hermenegildo, R

    M.V. Hermenegildo, R. Warren, and S. K. Debray. 1992. Global Flow Analysis as a Practical Compilation Tool.Journal of Logic Programming13, 4 (August 1992), 349–367. doi:10.1016/0743-1066(92)90053-6

    1992 doi

  33. [41]

    Zixin Huang, Jacob Laurel, Saikat Dutta, and Sasa Misailovic. 2025. AURA: Precise Abstract Interpretation ofProba- bilistic Programs with Interval Data Uncertainty. InStatic Analysis: 32nd International Symposium, SAS 2025, Singapore, Singapore, October 13–14, 2025, Proceeding...

    2025 doi

  34. [42]

    Jesse Hughes and Bart Jacobs. 2004. Simulations in coalgebra.Theoretical Computer Science327, 1 (2004), 71–108. doi:10.1016/j.tcs.2004.07.022 Special Issue on CMCS’03

    2004 doi

  35. [43]

    Andreas Humenberger, Maximilian Jaroschek, and Laura Kovács. 2017. Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences(ISSAC ’17). 221–228. doi:10.1145/3087604.3087623

    2017

  36. [45]

    Pierre Hyvernat. 2014. A Linear Category of Polynomial Functors (extensional part).Logical Methods in Computer ScienceVolume 10, Issue 2 (May 2014). doi:10.2168/lmcs-10(2:2)2014

    2014 doi

  37. [46]

    2016.Introduction to Coalgebra: Towards Mathematics of States and Observation

    Bart Jacobs. 2016.Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge University Press. doi:10.1017/cbo9781316823187

    2016 doi

  38. [47]

    Maxime Jacquemin, Fonenantsoa Maurica, Nikolai Kosmatov, Julien Signoles, and Franck Védrine. 2019. Abstract Compilation for Verification of Numerical Accuracy Properties. arXiv:1911.10930 https://arxiv.org/abs/1911.10930

    2019 arXiv

  39. [48]

    Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs

  40. [49]

    Gallagher, Manuel V

    Bishoksan Kafle, John P. Gallagher, Manuel V. Hermenegildo, Maximiliano Klemen, Pedro Lopez-Garcia, and José F. Morales. 2021. Regular Path Clauses and their Application in Solving Loops. InHCVS. doi:10.4204/EPTCS.344.3

    2021 doi

  41. [50]

    Shin-ya Katsumata, Xavier Rival, and Jérémy Dubut. 2023. A Categorical Framework for Program Semantics and Semantic Abstraction. In39th Conference on Mathematical Foundations of Programming Semantics (MFPS XXXIX). doi:10.46298/entics.12288

    2023 doi

  42. [51]

    Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, and Thomas Reps. 2017. Compositional Recurrence Analysis Revisited.SIGPLAN Not.52, 6 (June 2017), 248–262. doi:10.1145/3140587.3062373

    2017

  43. [52]

    Zachary Kincaid, Jason Breck, John Cyphert, and Thomas W. Reps. 2019. Closed forms for numerical loops.Proc. ACM Program. Lang.3, POPL (2019), 55:1–55:29. doi:10.1145/3290368

    2019 doi

  44. [53]

    Zachary Kincaid, John Cyphert, Jason Breck, and Thomas W. Reps. 2018. Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang.2, POPL (2018), 54:1–54:33. doi:10.1145/3158142

    2018 doi

  45. [54]

    Zachary Kincaid, Nicolas Koh, and Shaowei Zhu. 2023. When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic.Proc. ACM Program. Lang.7, POPL (2023), 1275–1307. doi:10.1145/3571237

    2023 doi

  46. [55]

    Zachary Kincaid and Shaowei Zhu. 2026. A Categorical Basis for Robust Program Analysis. InPLDI. doi:10.1145/3808307

    2026 doi

  47. [56]

    2007.Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema

    Laura Kovács. 2007.Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. Ph. D. Dissertation. RISC, Johannes Kepler University Linz. https://www3.risc.jku.at/publications/ download/risc_3274/ThesisKovacsSubmitted.pdf Advisors: ...

    2007

  48. [57]

    Laura Kovács. 2008. Reasoning Algebraically About P-Solvable Loops. InTools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS (Lecture Notes in Computer Science, Vol. 4963). Springer, Abstract Compilation as Abstraction of Operat...

    2008 doi

  49. [58]

    Satoshi Kura, Hiroshi Unno, and Takeshi Tsukada. 2026. Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification. InPLDI. doi:10.1145/3808348

    2026 doi

  50. [59]

    Joachim Lambek. 1968. A fixpoint theorem for complete categories.Mathematische Zeitschrift103, 2 (1968), 151–161. doi:10.1007/bf01110627

    1968 doi

  51. [60]

    Le Metayer

    D. Le Metayer. 1988. ACE: An Automatic Complexity Evaluator.TOPLAS(1988). doi:10.1145/42190.42347

    1988

  52. [61]

    Lehmann and Michael B

    Daniel J. Lehmann and Michael B. Smyth. 1981. Algebraic Specification of Data Types: a Synthetic Approach. Mathematical Systems Theory14, 1 (Dec. 1981), 97–139. doi:10.1007/bf01752392

    1981 doi

  53. [62]

    Matthieu Lemerre. 2023. SSA Translation Is an Abstract Interpretation.Proceedings of the ACM on Programming Languages7, POPL (2023), 1895–1924. doi:10.1145/3571258

    2023 doi

  54. [63]

    Dorian Lesbre and Matthieu Lemerre. 2024. Compiling with Abstract Interpretation.Proceedings of the ACM on Programming Languages8, PLDI (2024), 368–393. doi:10.1145/3656392

    2024 doi

  55. [64]

    Nils Lommen and Jürgen Giesl. 2023. Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs. InFroCos. doi:10.1007/978-3-031-43369-6_1

    2023 doi

  56. [65]

    Lopez-Garcia, L

    P. Lopez-Garcia, L. Darmawan, M. Klemen, U. Liqat, F. Bueno, and M.V. Hermenegildo. 2018. Interval-based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption.TPLP18, 2 (March 2018), 167–223. doi:10.1016/j.scico.2005.02.006

    2018 doi

  57. [66]

    Lopez-Garcia, M

    P. Lopez-Garcia, M. Klemen, U. Liqat, and M.V. Hermenegildo. 2016. A General Framework for Static Profiling of Parametric Resource Usage. InICLP. doi:10.1017/S1471068416000442

    2016 doi

  58. [67]

    Ernest G. Manes. 1976.Algebraic Theories. Springer New York. doi:10.1007/978-1-4612-9860-1

    1976 doi

  59. [68]

    Erik Meijer, Maarten Fokkinga, and Ross Paterson. 1991. Functional programming with bananas, lenses, envelopes and barbed wire. InFunctional Programming Languages and Computer Architecture (FPLCA), John Hughes (Ed.). Springer Berlin Heidelberg, 124–144. doi:10.1007/3540543961_7

    1991 doi

  60. [69]

    Eugenio Moggi. 1991. Notions of Computation and Monads.Information and Computation93, 1 (1991), 55–92. doi:10.1016/0890-5401(91)90052-4 Special Issue on LiCS’89

    1991 doi

  61. [70]

    Navas, E

    J. Navas, E. Mera, P. Lopez-Garcia, and M.V. Hermenegildo. 2007. User-Definable Resource Bounds Analysis for Logic Programs. In23rd International Conference on Logic Programming (ICLP’07) (Lecture Notes in Computer Science, Vol. 4670). Springer, 348–363. doi:10.1007/978-3-540-...

    2007 doi

  62. [71]

    Flemming Nielson. 1985. Tensor Products Generalize the Relational Data Flow Analysis Method. InProc. Fourth Hungarian Computer Science Conference. 211–225

    1985

  63. [72]

    Nikhil Pimpalkhare and Zachary Kincaid. 2024. Semi-linear VASR for Over-Approximate Semi-linear Transition System Reachability. InInternational Conference Reachability Problems (RP), Laura Kovács and Ana Sokolova (Eds.). Springer Nature Switzerland, Cham, 154–166. doi:10.1007/...

    2024 doi

  64. [73]

    G.D. Plotkin. 1977. LCF considered as a programming language.Theoretical Computer Science5, 3 (1977), 223–255. doi:10.1016/0304-3975(77)90044-5

    1977 doi

  65. [74]

    Puebla, E

    G. Puebla, E. Albert, and M.V. Hermenegildo. 2006. Abstract Interpretation with Specialized Definitions. InThe 13th International Static Analysis Symposium (SAS’06) (LNCS, 4134). Springer, 107–126. doi:10.1007/11823230_8

    2006 doi

  66. [75]

    Puebla and M.V

    G. Puebla and M.V. Hermenegildo. 2003. Abstract Specialization and its Applications. InACM Partial Evaluation and Semantics based Program Manipulation (PEPM’03). ACM Press, 29–43. doi:10.1145/777388.777393 Invited talk

    2003

  67. [76]

    Rosendahl

    M. Rosendahl. 1989. Automatic Complexity Analysis. InFPCA. doi:10.1145/99370.99381

    1989

  68. [77]

    Rossignoli and F

    S. Rossignoli and F. Spoto. 2006. Detecting Non-Cyclicity by Abstract Compilation into Boolean Functions. In7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’06). doi:10.1007/11609773_7

    2006 doi

  69. [78]

    Louis Rustenholz, Maximiliano Klemen, Miguel Ángel Carreira-Perpiñán, and Pedro López-García. 2024. A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs.TPLP24, 6 (November 2024), 1163–1207. doi:10.1017/S1471068424000413

    2024 doi

  70. [79]

    Hermenegildo

    Louis Rustenholz, Pedro Lopez-Garcia, and Manuel V. Hermenegildo. 2026. Abstractions of Sequences, Functions and Operators.Int’l. Journal on Software Tools for Technology Transfer(March 2026). doi:10.1007/s10009-026-00843-3 Special issue on CSV’25

    2026 doi

  71. [80]

    Morales, and Manuel V

    Louis Rustenholz, Pedro Lopez-Garcia, José F. Morales, and Manuel V. Hermenegildo. 2024. An Order Theory Framework of Recurrence Equations for Static Cost Analysis - Dynamic Inference of Non-Linear Inequality Invariants. InProceedings of the 31st Static Analysis Symposium (SAS...

    2024 doi

  72. [81]

    Takahiro Sanada, Yoàv Montacute, Kittiphon Phalakarn, and Ichiro Hasuo. 2026. A Coalgebraic Dijkstra Algorithm. arXiv:2605.22149 [cs.DS]

    2026 arXiv

  73. [82]

    Serrano, P

    A. Serrano, P. Lopez-Garcia, and M.V. Hermenegildo. 2014. Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types.TPLP, ICLP’14 Special Issue14, 4-5 (2014), 739–754. doi:10.1017/S147106841400057X 30 Louis Rustenholz et al

    2014 doi

  74. [83]

    Ana Sokolova. 2011. Probabilistic systems coalgebraically: A survey.Theoretical Computer Science412, 38 (2011), 5095–5110. doi:10.1016/j.tcs.2011.05.008 CMCS Tenth Anniversary Meeting

    2011 doi

  75. [84]

    Steffen, C

    B. Steffen, C. Barry Jay, and M. Mendler. 1992. Compositional characterization of observable program properties. RAIRO - Theoretical Informatics and Applications26, 5 (1992), 403–424. doi:10.7146/dpb.v19i328.6718

    1992 doi

  76. [85]

    M. H. van Emden and R. A. Kowalski. 1976. The Semantics of Predicate Logic as a Programming Language.Journal of the ACM23 (October 1976), 733–742. doi:10.1145/321978.321991

    1976

  77. [86]

    Daniele Varacca and Glynn Winskel. 2006. Distributing probability over non-determinism.Mathematical Structures in Computer Science16, 1 (Feb. 2006), 87–113. doi:10.1017/s0960129505005074

    2006 doi

  78. [87]

    Chenglin Wang and Fangzhen Lin. 2023. Solving Conditional Linear Recurrences for Program Verification: The Periodic Case.Proc. ACM Program. Lang.7, OOPSLA1 (2023), 28–55. doi:10.1145/3586028

    2023 doi

  79. [88]

    Hermenegildo

    Warren and M. Hermenegildo. 1988.On the Practicality of Global Flow Analysis of Logic Programs. Technical Report ACA-126-88. Microelectronics and Computer Technology Corporation (MCC), Austin, TX 78759

    1988

  80. [89]

    category without axioms

    B. Wegbreit. 1975. Mechanical Program Analysis.Commun. ACM18, 9 (September 1975), 528–539. doi:10.1145/361002. 361016 Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis 31 A Additional Preliminary Material This appendix contains additional prel...

    1975 doi

  81. [2019]

    ACM Program

    The future is ours: prophecy variables in separation logic.Proc. ACM Program. Lang.4, POPL, Article 45 (Dec. 2019), 32 pages. doi:10.1145/3371113

    2019 doi

  82. [2022]

    Solving Invariant Generation for Unsolvable Loops. InSAS. Springer, 19–43. doi:10.1007/978-3-031-22308-2_3

    doi

Pith tools

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