Pith. sign in

REVIEW 3 major objections 6 minor 3 cited by

Formal verification must become cumulative: synthesize contracts and proofs once, then reuse them across systems, with LLMs proposing matches and symbolic logic enforcing soundness.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-03 05:11 UTC pith:X6AGZYP5

load-bearing objection A clearly written vision paper that honestly disclaims implementation, but whose central 'symbolic matching ensures formal soundness' claim is undefined and unconnected to the semantic theory in Section 4—worth a workshop, not a research venue. the 3 major comments →

arxiv 2602.02881 v2 pith:X6AGZYP5 submitted 2026-02-02 cs.SE cs.AI

Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics

Arshad Beg , Diarmuid O'Donoghue , Rosemary Monahan This is my paper
classification cs.SE cs.AI
keywords formal verificationcontract synthesisartifact reuselarge language modelsgraph matchingsemantic embeddingsUnifying Theories of Programmingtheory of institutions
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The paper is a vision statement, not a finished system: its authors assert that the next generation of formal verification should work like a growing knowledge base rather than a series of isolated proof efforts. They propose the Learning-Infused Formal Reasoning (LIFR) framework, in which large language models provide semantic embeddings while the symbolic structure of typed graphs, matched approximately, keeps reuse formally sound. To make reuse trustworthy across different notations and abstraction levels, they ground the framework in unifying semantic theories so that a correct contract in one formalism can be migrated to another without losing meaning. The payoff, if the vision holds, is that verification effort accumulates: what is proved once becomes reusable capital for proving the next system.

Core claim

On the paper's own terms, the central discovery is a proposed architecture rather than a proven result: verification artifacts—programs, specifications, proofs—can be treated as typed, attributed graphs; LLM-derived embeddings add semantic information to graph nodes; and approximate graph matching combines structure with semantic similarity to find candidate correspondences between artifacts. The paper claims this hybrid can achieve principled reuse because the graph layer enforces formal constraints while the LLM only suggests associations, and it argues that the Unifying Theories of Programming and the Theory of Institutions supply the semantic substrate needed to justify such matches and

What carries the argument

The load-bearing mechanism is the three-step reuse pipeline: (1) graph construction, which lifts verification artifacts into typed, attributed graphs whose nodes are semantic entities and whose edges are relations like dataflow, refinement, or implication; (2) semantic enrichment, in which LLM-derived embeddings attach vector representations of textual and symbolic meaning to nodes; and (3) approximate graph matching, which finds alignments by combining structural consistency with embedding proximity. The paper pairs this with a semantic-faithfulness layer built from the Unifying Theories of Programming and the Theory of Institutions, whose satisfaction-preserving morphisms are meant to let

Load-bearing premise

The vision rests on the untested assumption that LLM embeddings plus graph structure can reliably identify semantic matches between artifacts written in different notations and at different abstraction levels while preserving the behavioral meaning needed for correctness.

What would settle it

A concrete test: take a set of pairs of contracts known to encode identical behavior—one pair in a state-based notation, one pair in a process-algebraic notation, one pair at different abstraction levels—run the proposed enrichment-and-matching pipeline, and measure whether it recovers the true correspondences and rejects unrelated pairs. If the hybrid matcher performs no better than character- or token-level similarity, or if it produces alignments that a symbolic refinement check then rejects for simple cases, the paper's central claim of sound, scalable reuse is falsified.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • If the reuse pipeline works, verification artifacts become reusable assets: a contract or proof developed for one system can be retrieved, adapted, and re-verified for a similar system rather than recreated from scratch.
  • LLM-generated contracts stop being one-shot outputs; with verifier feedback feeding back into generation, synthesis becomes a convergence process that suppresses hallucinations.
  • A tool-neutral semantic foundation would let the same specification be translated between notations and verification environments while preserving its meaning, enabling cross-tool and cross-language verification.
  • The separation of roles—LLM as semantic oracle, graph structure as enforcer of formal constraints—is the paper's proposed answer to the trust problem: machine learning guides search without being trusted for correctness.
  • Verification shifts from a one-off correctness check to a cumulative discipline in which past work accelerates future assurance.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • An implication the paper leaves implicit: the framework's viability hinges on datasets that do not yet exist—aligned corpora connecting real requirements to verified specifications with recorded solver outcomes. Until such corpora are built, the matching-and-reuse claims cannot be empirically tested.
  • A natural testable extension is to benchmark the hybrid matcher against existing verification artifact repositories, measuring whether it recovers known semantic equivalences more reliably than surface-level textual or structural matching alone.
  • The separation-of-roles design could generalize beyond verification to any correctness-critical AI application where a statistical model proposes candidates and a symbolic layer certifies them.
  • If the semantic-matching step can be certified by institution morphisms, the same machinery might enable automated, provably correct translation between formal specification languages—a capability that currently requires manual theorem-proving expertise.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 6 minor

Summary. The paper is a vision paper that proposes 'Learning-Infused Formal Reasoning' (LIFR), a long-term research agenda for integrating large language models with graph-based representations and formal semantic foundations (UTP, institutions) to support automated contract synthesis, semantic artifact reuse, and cross-formalism interoperability. The central claim, stated in the abstract, is that a hybrid of LLM-derived semantic guidance and symbolic/graph-based matching can ensure formal soundness in the reuse of verification artifacts, while the authors report on their ongoing work and position prior publications as the empirical foundation. The paper is organized into three threads and includes a conceptual architecture, a reuse pipeline diagram, and a discussion of open challenges, but it contains no implementation, experiments, or formal derivations.

Significance. If the LIFR vision is realized, it would make a meaningful contribution by addressing real bottlenecks in formal methods: the high cost of specification synthesis, the lack of systematic reuse of verification artifacts, and the poor interoperability between heterogeneous formalisms. The paper's emphasis on using institution morphisms and UTP refinement to provide semantic governance is a plausible and valuable direction. The main strengths are the clear articulation of the three-thread agenda, the informed discussion of relevant prior work (including the authors' own studies), and the identification of concrete open challenges such as dataset quality, prompt instability, and traceability. The paper is honest about being a proposal rather than a completed system. However, the scientific contribution is currently conditional: the load-bearing claim of 'symbolic matching ensures formal soundness' is not defined or derived, so the significance of the reuse pipeline remains unclear.

major comments (3)
  1. [Abstract, §3.2, §6] The central claim that 'symbolic matching ensures formal soundness' is undefined. Section 3.2 models verification artifacts as typed, attributed graphs and proposes approximate graph matching that combines structure with LLM embeddings. But structural graph similarity does not, by itself, preserve behavioral semantics. No definition is given of what 'symbolic matching' must preserve, and no theorem or proof obligation is stated that would connect a graph alignment to a satisfaction-preserving morphism or a refinement in the sense of §4. Since the conclusion (Section 6) repeats the assertion that transferred artifacts preserve correctness guarantees, this is not a minor omission but a missing cornerstone of the proposal.
  2. [§3.2, §4, Fig. 2] The reuse pipeline (Figure 2) and the theoretical infrastructure of Section 4 are never connected. Section 4 introduces UTP and institutions and argues that AI agents should operate under 'healthiness conditions, refinement laws, and satisfaction-preserving mappings,' but there is no argument that the candidate alignments produced by approximate graph matching correspond to any such mapping. To make the soundness claim defensible, the paper must either (a) define a semantic preservation condition for the graph encoding and matching relation, or (b) describe how an alignment is checked against an institution morphism or UTP refinement before reuse, and justify that the checking is sound and complete (or at least sound). Without this, the 'semantic governance' layer remains aspirational and disconnected from the matching algorithm.
  3. [§3.2, §5] The paper acknowledges that reuse is a problem of 'semantic matching under partial equivalence and abstraction,' yet the abstract and conclusion claim soundness in absolute terms. This tension is never resolved. If matches are approximate and equivalence is partial, what exactly is guaranteed? A soundness guarantee for reuse must account for the abstraction levels of the source and target artifacts; merely stating that graph structure enforces 'global relational and type constraints' (§3.2) is insufficient. The same concern is implicitly acknowledged in Section 5, which admits that 'true semantic correctness, refinement preservation, and scalability cannot be measured' without better datasets—but the paper does not consider this a threat to the soundness claim. A revision should either weaken the soundness claim to one about structural constraints, or provide a precise formulation of wha
minor comments (6)
  1. [Abstract] Minor typo: 'must builds towards' should be 'must build toward'.
  2. [References] The in-text citation 'Earlier work on Aris Pitu et al. (2013)' appears garbled; the reference list entry lists 'Pitu M' as the first author, so the in-text name should be corrected. Similarly, 'Ajankovil et al. (2021)' may be a misspelling of the first author name in the reference 'Ajankovil KG'.
  3. [§4.3] There is a missing space: 'We knowmodel-checkers' should read 'We know model-checkers'.
  4. [§6] Typo: 'candidate aligns' should be 'candidate alignments'.
  5. [§3.2] The phrase 'Path-expression–based views of graphs' is not defined or referenced; it would benefit from a brief explanation or a citation so that the reader can understand how this connects to the reuse pipeline.
  6. [References] Several citations rely on the authors' own prior work, including Beg et al. (2025b), which is listed as 'submitted' with a Zenodo preprint. While this is acceptable for a vision paper, its use as the primary empirical foundation should be explicitly qualified, and the paper should clarify which versions are peer-reviewed.

Circularity Check

0 steps flagged

No significant circularity: the paper is a vision/position statement with no fitted parameters or derivation chain whose conclusions reduce to its inputs.

full rationale

The manuscript is an explicitly forward-looking vision paper. It contains no equations, no fitted parameters, and no empirical predictions derived from data; the abstract's claim that 'symbolic matching ensures formal soundness' is a programmatic assertion, not a result obtained by reducing one quantity to another. The reuse pipeline in Section 3 is described as a proposal ('we propose modelling verification artefacts as typed, attributed graphs...'), and Section 2 likewise states it is 'intentionally presented as a conceptual proposal rather than a realised system.' The heavy use of the authors' own prior work (Beg et al. 2025a,b; Beg 2016; Farrell 2017; Reynolds 2023) is contextual: it motivates open problems and cites an internal survey for the difficulty of LLM-based formalisation. Those citations are not used to import a uniqueness theorem or to force the choice of graph matching; they supply background and prior empirical observations. The conclusion's assurance that refinement relations 'ensure that transferred artifacts preserve correctness guarantees' is asserted as future architecture rather than derived in this paper. The skeptic's complaint—that no satisfaction-preserving morphism or semantic preservation condition connects approximate graph matching to institution morphisms—is a gap in evidence and a correctness risk, not a circular reduction. No step of the paper's reasoning is equivalent to its own input by construction, so the circularity score is 0.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 0 invented entities

No free parameters or invented entities appear; the ledger records domain assumptions on which the proposed LIFR architecture depends. All are either explicitly flagged as assumptions in the text or inherited from prior work without new validation.

axioms (4)
  • domain assumption LLM-derived embeddings can serve as semantic oracles that suggest correspondences between graph nodes across heterogeneous notations and abstraction levels.
    Section 3.2 states that LLMs 'serve as semantic oracles' and that embeddings enrich graph nodes; no quantitative evidence is provided for verification artifacts.
  • domain assumption Approximate graph matching that combines structural consistency with embedding proximity finds reuse alignments that preserve behavioral meaning.
    This is the core of the proposed reuse pipeline (Section 3.2, Figure 2); soundness of the matches is assumed rather than proven.
  • domain assumption UTP and the Theory of Institutions provide a sufficiently expressive and mechanizable semantic substrate for AI-generated artifacts across ACSL, Event-B, TLA+, and CSP.
    Section 4 invokes Woodcock, Goguen and Burstall, and Reynolds; no new institution or morphism is defined or validated in this paper.
  • domain assumption LLM prompt instability can be controlled by grammar-restricted decoding and tool-specific ASTs without losing specification coverage.
    Section 5 proposes this as a future direction; no experiments support the claim.

pith-pipeline@v1.3.0-alltime-deepseek · 11064 in / 10467 out tokens · 113963 ms · 2026-08-03T05:11:13.413199+00:00 · methodology

0 comments
read the original abstract

This paper articulates a long-term research vision for formal methods at the intersection with artificial intelligence, outlining multiple conceptual and technical dimensions and reporting on our ongoing work toward realising this vision. It advances a forward-looking perspective on the next generation of formal methods based on the integration of automated contract synthesis, semantic artifact reuse, and refinement-based theory. We argue that future verification systems must builds towards individual correctness proofs toward a cumulative, knowledge-driven paradigm in which specifications, contracts, and proofs are continuously synthesised and transferred across systems. To support this shift, we outline a hybrid framework combining large language models with graph-based representations to enable scalable semantic matching and principled reuse of verification artifacts. Learning-based components provide semantic guidance across heterogeneous notations and abstraction levels, while symbolic matching ensures formal soundness. Grounded in compositional reasoning, this vision points toward verification ecosystems that evolve systematically, leveraging past verification efforts to accelerate future assurance.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Graph Construction and Matching for Imperative Programs using Neural and Structural Methods

    cs.SE 2026-04 unverdicted novelty 5.0

    A pipeline converts programs with annotations into typed attributed graphs using AST parsing and neural embeddings to support verification artefact reuse across languages.

  2. Graph Construction and Matching for Imperative Programs using Neural and Structural Methods

    cs.SE 2026-04 unverdicted novelty 5.0

    A multi-language pipeline converts C/ACSL, Java/JML, and Dafny programs into typed attributed graphs combining AST structure with SentenceTransformer and CodeBERT embeddings.

  3. Graph Construction and Matching for Imperative Programs using Neural and Structural Methods

    cs.SE 2026-04 unverdicted novelty 4.0

    A pipeline builds consistent typed attributed graphs from imperative programs and annotations in multiple languages by combining structural parsing with semantic embeddings from code models.

Reference graph

Works this paper leans on

40 extracted references · 8 canonical work pages · cited by 1 Pith paper

  1. [1]

    sn-basic.bst

    FUNCTION identify.basic.version "sn-basic.bst" " [2024/07/19 v1.1 bibliography style]" * top ENTRY address archive author booktitle chapter doi edition editor eid eprint howpublished institution journal key keywords month note number organization pages publisher school series title type url volume year archivePrefix primaryClass adsurl adsnote version lab...

    2024

  2. [2]

    write newline

    " write newline "" before.all 'output.state := FUNCTION add.period duplicate empty 'skip "." * add.blank if FUNCTION if.digit duplicate "0" = swap duplicate "1" = swap duplicate "2" = swap duplicate "3" = swap duplicate "4" = swap duplicate "5" = swap duplicate "6" = swap duplicate "7" = swap duplicate "8" = swap "9" = or or or or or or or or or FUNCTION ...

  3. [3]

    In: International Conference on Computational Creativity (ICCC)

    Ajankovil KG, O'Donoghue D, Monahan R (2021) Creating new program proofs by combining abductive and deductive reasoning. In: International Conference on Computational Creativity (ICCC)

    2021

  4. [4]

    Ali SJ, Naganathan V, Bork D (2024) Establishing traceability between natural language requirements and software artifacts by combining RAG and llms. In: Maass W, Han H, Yasar H, et al (eds) Conceptual Modeling - 43rd International Conference, ER 2024, Pittsburgh, PA, USA, October 28-31, 2024, Proceedings, Lecture Notes in Computer Science, vol 15238. Spr...

    doi:10.1007/978-3-031-75872-0 2024

  5. [5]

    state-rich

    Beg A (2016) Translating from "state-rich" to "state poor" process algebras. PhD thesis, Trinity College Dublin, Ireland, ://hdl.handle.net/2262/82894

    2016

  6. [6]

    In: FIT '10, 8th International Conference on Frontiers of Information Technology, Islamabad, Pakistan, December 21-23, 2010

    Beg A, Butterfield A (2010) Linking a state-rich process algebra to a state-free algebra to verify software/hardware implementation. In: FIT '10, 8th International Conference on Frontiers of Information Technology, Islamabad, Pakistan, December 21-23, 2010. ACM , p 47, doi:10.1145/1943628.1943675, ://doi.org/10.1145/1943628.1943675

    arXiv 2010

  7. [7]

    In: 9th IEEE International Conference on Open Source Systems and Technologies (ICOSST 2015), Lahore, Pakistan., IEEE Digital Library, pp 16--23

    Beg A, Butterfield A (2015) Development of a prototype translator from circus to cspm. In: 9th IEEE International Conference on Open Source Systems and Technologies (ICOSST 2015), Lahore, Pakistan., IEEE Digital Library, pp 16--23

    2015

  8. [8]

    Beg A, O'Donoghue D, Monahan R (2025 a ) Leveraging LLMs for formal software requirements: Challenges and prospects. In: Proceedings of the 7th International Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis (OVERLAY) @ ECAI 2025, Bologna, Italy, ://overlay.uniud.it/workshop/2025/papers/beg-etal.pdf

    2025

  9. [9]

    Journal of Software Testing, Verification and Reliability doi:10.5281/zenodo.17772835, ://doi.org/10.5281/zenodo.17772835, submitted; Version v1 available on Zenodo

    Beg A, O'Donoghue D, Monahan R (2025 b ) Traceable and verifiable software requirements: A synthesis of ai-enabled formal methods. Journal of Software Testing, Verification and Reliability doi:10.5281/zenodo.17772835, ://doi.org/10.5281/zenodo.17772835, submitted; Version v1 available on Zenodo

    doi:10.5281/zenodo.17772835 2025

  10. [10]

    Butterfield A, Tuong F (2023) Applying formal verification to an open-source real-time operating system. In: Bowen JP, Li Q, Xu Q (eds) Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday, Lecture Notes in Computer Science, vol 14080. Springer, pp 348--366, doi:10.1007/978-3-031-40436-8\_13, ://d...

    work page doi:10.1007/978-3-031-40436-8 2023

  11. [11]

    PhD thesis, Maynooth University

    Farrell M (2017) Event-b in the institutional framework: defining a semantics, modularisation constructs and interoperability for a specification language. PhD thesis, Maynooth University

    2017

  12. [12]

    Farrell M, Monahan R, Power JF (2017) An Institution for Event-B . In: Rec. Trends Alg. Dev. Tech., Springer, pp 104--119, doi:10.1007/978-3-319-72044-9_8

    work page doi:10.1007/978-3-319-72044-9_8 2017

  13. [13]

    In: Form

    Foster S, Baxter J, Cavalcanti A, et al (2018) Automating verification of state machines with reactive designs and Isabelle/UTP . In: Form. Asp. Comp. Soft., Springer, pp 137--155

    2018

  14. [14]

    Science of Computer Programming 197:102510

    Foster S, Baxter J, Cavalcanti A, et al (2020) Unifying semantic foundations for automated verification tools in isabelle/utp. Science of Computer Programming 197:102510. doi:https://doi.org/10.1016/j.scico.2020.102510, ://www.sciencedirect.com/science/article/pii/S0167642320301192

    arXiv 2020

  15. [15]

    In: Ogata K, Lawford M, Liu S (eds) Formal Methods and Software Engineering

    Gadia S, Artho C, Bloom G (2016) Verifying nested lock priority inheritance in rtems with java pathfinder. In: Ogata K, Lawford M, Liu S (eds) Formal Methods and Software Engineering. Springer International Publishing, Cham, pp 417--432, doi:10.1007/978-3-319-47846-3_26

    work page doi:10.1007/978-3-319-47846-3_26 2016

  16. [16]

    J ACM 39(1):95–146

    Goguen JA, Burstall RM (1992 a ) Institutions: abstract model theory for specification and programming. J ACM 39(1):95–146. doi:10.1145/147508.147524, ://doi.org/10.1145/147508.147524

    arXiv 1992

  17. [17]

    J ACM 39(1):95--146

    Goguen JA, Burstall RM (1992 b ) Institutions: abstract model theory for specification and programming . J ACM 39(1):95--146

    1992

  18. [18]

    Innov Syst Softw Eng 18(4):567--580

    Hammer A, Cauwels M, Hertz B, et al (2022) Integrating runtime verification into an automated UAS traffic management system. Innov Syst Softw Eng 18(4):567--580. doi:10.1007/S11334-021-00407-5, ://doi.org/10.1007/s11334-021-00407-5

    work page doi:10.1007/s11334-021-00407-5 2022

  19. [19]

    In: Math

    Hoare CAR (1997) Unified theories of programming . In: Math. Meth. Prog. Dev. Springer, p 313--367

    1997

  20. [20]

    Ingrand F (2019) Recent trends in formal validation and verification of autonomous robots software . In: Rob. Comput. IEEE, pp 321--328, doi:10.1109/IRC.2019.00059

    arXiv 2019

  21. [21]

    In: ETFA2011, pp 1--9, doi:10.1109/ETFA.2011.6058982

    Iyenghar P, Pulvermueller E, Westerkamp C (2011) Towards model-based test automation for embedded systems using uml and utp. In: ETFA2011, pp 1--9, doi:10.1109/ETFA.2011.6058982

    arXiv 2011

  22. [22]

    Lippolis AS, Klironomos A, Milon - Flores DF, et al (2023) Enhancing entity alignment between wikidata and artgraph using llms. In: Bikakis A, Ferrario R, Jean S, et al (eds) Proceedings of the International Workshop on Semantic Web and Ontology Design for Cultural Heritage co-located with the International Semantic Web Conference 2023 (ISWC 2023), Athens...

    2023

  23. [23]

    ACM Comput Surv 52(5):1--41

    Luckcuck M, Farrell M, Dennis LA, et al (2019) Formal specification and verification of autonomous robotic systems: a survey . ACM Comput Surv 52(5):1--41

    2019

  24. [24]

    CoRR abs/2501.08686

    Ma C, Chakrabarti S, Khan A, et al (2025) Knowledge graph-based retrieval-augmented generation for schema matching. CoRR abs/2501.08686. doi:10.48550/ARXIV.2501.08686, ://doi.org/10.48550/arXiv.2501.08686, https://arxiv.org/abs/2501.08686 2501.08686

    Pith/arXiv arXiv doi:10.48550/arxiv.2501.08686 2025

  25. [25]

    In: Intell

    Miyazawa A, Ribeiro P, Li W, et al (2017) Automatic property checking of robotic applications . In: Intell. Rob. Syst., IEEE, pp 3869--3876

    2017

  26. [26]

    Softw Syst Mod 18(5):3097--3149

    Miyazawa A, Ribeiro P, Li W, et al (2019) RoboChart: modelling and verification of the functional behaviour of robotic applications . Softw Syst Mod 18(5):3097--3149

    2019

  27. [27]

    Springer

    Mosses PD (2004) CASL reference manual: the complete documentation of the common algebraic specification language . Springer

    2004

  28. [28]

    In: International Conference on Computational Creativity (ICCC)

    O'Donoghue D, Abgaz Y, Hurley D, et al (2015) Stimulating and simulating creativity with dr inventor. In: International Conference on Computational Creativity (ICCC). Brigham Young University, USA

    2015

  29. [29]

    In: PICS-Publication Series of the Institute of Cognitive Science, vol 1

    O’Donoghue D, Monahan R, Grijincu D, et al (2014) Creating formal specifications with analogical reasoning. In: PICS-Publication Series of the Institute of Cognitive Science, vol 1. Institute of Cognitive Science

    2014

  30. [30]

    In: Proceedings Artificial Intelligence for Formal Methods (AI4FM)

    Pitu M, Grijincu D, Li P, et al (2013) Ar \' s: Analogical reasoning for reuse of implementation & specification. In: Proceedings Artificial Intelligence for Formal Methods (AI4FM). Department of Computer Science, Heriot-Watt University

    2013

  31. [31]

    PhD thesis, National University of Ireland Maynooth

    Reynolds C (2023) Machine-assisted proofs for institutions. PhD thesis, National University of Ireland Maynooth

    2023

  32. [32]

    Springer

    Sannella D, Tarlecki A (2012) Foundations of algebraic specification and formal software development . Springer

    2012

  33. [33]

    Strecker M (2007) Modeling and verifying graph transformations in proof assistants. In: Mackie I, Plump D (eds) Proceedings of the Fourth International Workshop on Computing with Terms and Graphs, TERMGRAPH@ETAPS 2007, Braga, Portugal, March 31, 2007, Electronic Notes in Theoretical Computer Science, vol 203. Elsevier, pp 135--148, doi:10.1016/J.ENTCS.200...

    work page doi:10.1016/j.entcs.2008.03.039 2007

  34. [34]

    In: International conference on applied engineering and natural sciences, pp 1050--1056

    Topsakal O, Akinci TC (2023) Creating large language model applications utilizing langchain: A primer on developing llm apps fast. In: International conference on applied engineering and natural sciences, pp 1050--1056

    2023

  35. [35]

    Tufek N, Thuluva AS, Just VP, et al (2024) Validating semantic artifacts with large language models. In: Mero \ n o - Pe \ n uela A, Corcho \' O , Groth P, et al (eds) The Semantic Web: ESWC 2024 Satellite Events - Hersonissos, Crete, Greece, May 26-30, 2024, Proceedings, Part I , Lecture Notes in Computer Science, vol 15344. Springer, pp 92--101, doi:10....

    work page doi:10.1007/978-3-031-78952-6 2024

  36. [36]

    Vandemoortele N, Steenwinckel B, Hoecke SV, et al (2024) Scalable table-to-knowledge graph matching from metadata using llms. In: Hassanzadeh O, Abdelmageed N, Cremaschi M, et al (eds) Proceedings of the Semantic Web Challenge on Tabular Data to Knowledge Graph Matching co-located with the 23rd International Semantic Web Conference (ISWC 2024), Baltimore,...

    2024

  37. [37]

    large language models: Competitors or partners in supporting virtual museums

    Vasic I, Fill HG, Quattrini R, et al (2025) Knowledge graphs vs. large language models: Competitors or partners in supporting virtual museums. ACM Journal on Computing and Cultural Heritage

    2025

  38. [38]

    In: Goldberg Y, Kozareva Z, Zhang Y (eds) Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing

    Wang B, Deng X, Sun H (2022) Iteratively prompt pre-trained language models for chain of thought. In: Goldberg Y, Kozareva Z, Zhang Y (eds) Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing. Association for Computational Linguistics, Abu Dhabi, United Arab Emirates, pp 2714--2730, doi:10.18653/v1/2022.emnlp-main.174, :...

    work page doi:10.18653/v1/2022.emnlp-main.174 2022

  39. [39]

    In: Bert D, Bowen JP, Henson MC, et al (eds) ZB 2002: Formal Specification and Development in Z and B

    Woodcock J, Cavalcanti A (2002) The semantics of circus. In: Bert D, Bowen JP, Henson MC, et al (eds) ZB 2002: Formal Specification and Development in Z and B. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 184--203, doi:10.1007/3-540-45648-1_10

    work page doi:10.1007/3-540-45648-1_10 2002

  40. [40]

    In: Boiten EA, Derrick J, Smith G (eds) Integrated Formal Methods

    Woodcock J, Cavalcanti A (2004) A tutorial introduction to designs in unifying theories of programming. In: Boiten EA, Derrick J, Smith G (eds) Integrated Formal Methods. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 40--66

    2004