Pith. sign in

REVIEW 6 major objections 4 minor 34 references

RE-oriented Model Development with LLM Support and Deduction-based Verification

T0 review · 6 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read This paper proposes LoRE+, an IDE-centred framework that converts LLM-assisted UML activity diagrams into equivalent PLTL specifications, verifies them with theorem provers, and generates Java/Python code skeletons.

desk verdict The pipeline is a sensible LLM+RE integration, but Claim 8's equivalence is checkably false: the Table 1 formulas don't enforce workflow order. read the letter →

arxiv 2506.08606 v1 pith:5SMSB6ZL submitted 2025-06-10 cs.SE

Radoslaw Klimek This is my paper
classification cs.SE MSC 68Q6068N30
keywords requirementsengineeringUMLactivitydiagramslargelanguagemodelspropositionallinear-timetemporallogicdeductiveverificationcodeskeletongenerationcorrectness-by-constructioncompositionalpatterns
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

Requirements engineering is dominated by informal natural-language scenarios, and going from those to a verified behavioural model is usually manual and error-prone. This paper proposes LoRE+, a framework in which an LLM first tags atomic activities and workflow structures in a use-case scenario, and those tagged structures are then assembled into activity diagrams that must follow six approved patterns: sequential composition, double sequence, conditional, conditional-without-else, parallel, and loop. For any such diagram the framework automatically produces an equivalent logical specification in propositional linear-time temporal logic (PLTL), checks the specification against required safety and liveness properties with theorem provers, and generates a Java or Python code skeleton. The central claim, stated as Claim 8, is that this pipeline is efficient and sound: pattern-to-formula translation is linear-time and sound, and the generated logical reasoning is time-efficient. If right, the approach turns the early design phase into a verified, correct-by-construction bridge from natural-language requirements to code skeletons.

What carries the argument

The machinery is the approved pattern set Π = {Seq, SeqSeq, Cond, Alt, Para, Loop} together with the fixed Σ table of PLTL properties assigned to each pattern (Table 1). Πscan maps a compositionally formed activity diagram to a pattern expression Wj, and ΠC expands Wj, using Σ, into a PLTL specification Lj; the paper cites [19] for the claim that ΠC is sound and linear-time. A second piece is the context-free grammar over these pattern names, which lets a parser-generator turn Wj into Java/Python skeletons. The case study's W(AD2) and L(AD2) show the two representations working on one nested car-insurance workflow.

What would settle it

Construct a nested activity diagram from the six patterns — for example, a loop whose body contains a conditional with a parallel branch — run Πscan and ΠC, and ask a PLTL model checker whether every model of the generated specification is a valid execution of the diagram; any violating model refutes the soundness claim.

Watch

Extended reading notes

Core claim

The paper's central claim is that a UML activity diagram built from a small set of composition patterns — Seq, SeqSeq, Cond, Alt, Para, Loop — carries enough structure that its entire behaviour can be captured exactly by a fixed table of PLTL formulas, one per pattern. The Πscan algorithm reads a compositionally formed diagram and emits a pattern expression Wj; the ΠC algorithm then expands Wj using the Σ table into a PLTL specification Lj that is logically equivalent to the diagram. Any generated specification can be handed to a theorem prover (or, after replacing temporal operators by quantifiers, a first-order prover) to test whether required properties such as liveness and safety follow from the specification. The same pattern expression feeds a context-free grammar and parser-generator pipeline that produces a compilable Java (or Python) skeleton whose control flow mirrors the workflow, with each activity as a stub function. The paper also claims, based on its case study, that one-shot LLM prompting is reliable enough to extract both the atomic activities and the nested pattern structures from natural-language scenarios, with human correction only occasional.

Load-bearing premise

That the six approved patterns and the fixed Σ table can express every workflow the framework will encounter, and that the ΠC translation from the earlier work is sound for every nested combination of those patterns.

Editorial extensions

If this is right

  • Every workflow that obeys the six patterns gets an automatically generated PLTL specification, so engineers can check safety and liveness requirements without writing temporal logic by hand.
  • Because the pattern expression Wj is also a regular expression over pattern names, code skeletons are generated from the same artefact that drives verification, keeping control flow consistent between model and code.
  • The equivalence claim means a failing requirement check is evidence that the workflow as modelled violates the property, not an artifact of translation, assuming ΠC is sound.
  • Since PLTL is more expressive than first-order logic, the same Σ table can be simplified by replacing temporal operators with quantifiers and reused with widely available first-order theorem provers.
  • The framework positions LLM output as a draft that is corrected against a fixed pattern grammar, which bounds the LLM's freedom and makes its output verifiable.

Reading between the lines

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

  • The paper's soundness claim inherits its force from the earlier ΠC result; if a future counterexample shows a nested mixture of the six patterns whose PLTL expansion admits a run the diagram forbids, the framework would need a larger pattern set or a revised Σ table.
  • A natural testable extension is to measure LLM extraction accuracy over a corpus of use-case scenarios, since the paper's reliability claim rests on a single case study without quantitative evaluation.
  • The same pattern-expression/grammar pipeline could generate other target languages or intermediate representations, such as BPMN or state machines, because the skeleton generator only depends on the grammar over pattern names.
  • The verification step could be strengthened by automatically generating counterexample traces from the theorem prover when a property fails, turning the Y/N hint into a debugging aid.
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

6 major / 4 minor

Summary. The paper describes a framework, LoRE+, that aims to integrate LLM-based extraction of activities and workflow structures from natural-language scenarios with formal deductive verification of the resulting UML activity diagrams. The workflow must conform to six predefined patterns (Seq, SeqSeq, Cond, Alt, Para, Loop), from which a logical specification in PLTL is automatically generated via a previously published algorithm, and the specification is then verified with theorem provers. The paper also describes a grammar-based generator of Java/Python program skeletons. The main claims are that the pattern set covers the needed UML activity diagrams, that the translation to PLTL is sound, and that the LLM-based extraction is sufficiently reliable. A case study of a car-insurance scenario is used to illustrate the pipeline, including a generated logical specification and a code skeleton.

Significance. If the correctness claims were established, the idea of using a small, expert-defined pattern set as the interface between LLM-generated models and deductive verification would be a useful and pragmatic contribution to requirements-engineering tool support. The paper also proposes a lightweight mechanism to generate compilable code skeletons from the same structural expressions. However, the central formal claim is not merely unproved but is demonstrably false as presented: the PLTL axioms in Table 1 do not enforce the intended workflow order, and several symbols used in the formulas are undefined. Because the correctness of the entire framework depends on this semantics, the current manuscript does not substantiate its main contribution, although the underlying concept appears salvageable with a corrected formal semantics and additional evidence.

major comments (6)
  1. [Section 3, Table 1 and Claim 8] The Seq pattern in Table 1 is not a sound encoding of sequential composition. For Seq(a1,a2), the listed conjuncts are ◇a1, □(a1 ⇒ ◇a2), and □¬(a1∧a2). On the trace a2;a1;a2 (a2 at position 0, a1 at position 1, a2 at position 2), all three formulas hold, yet the trace does not execute a1 before a2. Thus the displayed semantics does not even enforce the basic order of a sequence, contradicting the claimed equivalence in Claim 8 and Remark 3. The same order problem affects the Cond, Alt, Para, and Loop patterns, whose given properties state liveness and mutual-exclusion conditions but do not constrain the relative order of the decision and its branches. The paper must provide a corrected semantics that genuinely reflects the control flow of each pattern.
  2. [Table 1 and Formula (5)] The symbols a1+, a1−, a2+, a2− used in Cond, Alt, and Loop (and in the generated specification L(AD2)) are never defined. The text introduces them informally as condition outcomes, but no formal semantics is given: they are not introduced as fresh propositions, no constraints such as a+ ⇔ a and ¬(a+∧a−) are stated, and the formulas in Table 1 are therefore not well-formed PLTL. The author must define these symbols and state the axioms that govern them before the claimed translation can be assessed.
  3. [Section 3, Claim 8] The soundness of the central transformation ΠC is delegated to a self-citation [19] and is not reproduced or proved in this manuscript. Even setting aside the concrete counterexample in Table 1, Claim 8 merely asserts soundness and linear-time complexity without a proof sketch or a machine-checked certificate. Given that the correctness of the entire verification pipeline rests on this transformation, the paper should either include a self-contained proof of the compositionality theorem for the corrected semantics or provide a formalization (e.g., in a proof assistant) that can be independently checked.
  4. [Section 6, Formula (6)] The paper claims deductive verification but does not report any actual verification result. Formula (6) states ⊢ Cn(L(AD2)) ⇒ r1∧r2, but no prover invocation, proof output, runtime, or even a yes/no answer is shown. The case study therefore demonstrates a plausible pipeline but not the claimed deduction-based verification. The author should run the presented specification through the named tools (e.g., InKreSAT, E, or Vampire) and report the actual outcomes and performance.
  5. [Section 4, Claim 3] Claim 3 states that the one-shot LLM-based extraction 'demonstrates remarkable reliability' and 'requires minimal human intervention', but no evaluation is provided. There is no benchmark, no sample size, no measurement of extraction accuracy, and no discussion of prompt variability or LLM version differences. The case study only shows one hand-tagged scenario. Without any empirical support, the claimed reliability is an unsupported assertion.
  6. [Section 3, after Remark 3] The statement 'PLTL logic is more expressive than First-Order Logic' is imprecise and, in the standard comparison over (N,<) with monadic predicates, not correct in the way the paper uses it; the expressiveness of LTL/PLTL relative to FO depends on the allowed operators and the signature. This claim is used to justify substituting FOL for PLTL in the testing workflow, so it should either be corrected with the appropriate qualification (e.g., Kamp's theorem with past operators) or removed.
minor comments (4)
  1. [Section 6, first paragraph] The parenthetical mapping of numbers to propositions defines symbols 1 through 24 without primes, but Formula (4) and Formula (5) use primed variables such as 16′, 20′, and 21′. The explanation that 'the prime symbol signifies copied variables treated as new atomic variables' appears only in passing and should be elaborated: each primed variable must be explicitly defined or generated by a clear rule.
  2. [Table 1] The angle-bracket notation ⟨a1, a2, 3a1, ...⟩ is not formally defined. It should be stated that ⟨φ1, ..., φk⟩ denotes the conjunction φ1 ∧ ... ∧ φk, or the notation should be replaced with a set or a conjunction of formulas.
  3. [Listing 3] The generated Java skeleton does not correspond to the pattern expression in Formula (4). For instance, the first activity in W(AD2) is activity 1 (DamageClaim), but the skeleton begins with a call to DamageVindication(), which is not in the mapping for activity 1. Without a clear explanation of how Listing 3 is derived from Formula (4), Claim 5 about automatic skeleton generation is hard to reproduce.
  4. [Definition 2] The grammar production ⟨Java-args⟩ → ε means that the generated skeleton contains only function names without arguments; the paper mentions experiments with actual arguments but does not show the needed extension of the grammar. A brief example of the extended grammar or a note that the extension is routine would improve clarity.

Circularity Check

2 steps flagged · score 6.0 of 10

The central soundness claim for the workflow-to-PLTL translation is inherited from the author's own prior work [19] and from Table 1's self-assigned pattern semantics, with no independent proof or benchmark in this paper.

  1. self citation load bearing [Section 3 (introductory paragraph; Claim 8)]
    "However, as demonstrated above [19, 22], the automatic generation of logical specifications is feasible for a certain class of models when activity diagrams are constructed in accordance with the composition principle... The transformation of structural workflows into logical specifications has linear time complexity and is sound [19]."

    The paper's strongest claim (Claim 8) is that the ΠC translation is efficient and sound. This is not proved or benchmarked in the manuscript; the proof is deferred to [19], the author's own prior journal paper, and the feasibility is also credited to [19, 22], which shares authorship. The pattern set and Σ formulas in Table 1 are likewise introduced 'following the work of [19]'. Thus the load-bearing logical core of the framework is accepted on the authority of the same author's prior work rather than being demonstrated here, so the claimed equivalence cannot be independently checked from the present text.

  2. self definitional [Section 3, Definition 1 / Table 1 and Claim 8]
    "The logical properties of predefined patterns from Formula (1) have been defined here, following the work of [19], in Table 1. ... The syntax and semantics of workflows are defined (Definition 1, Table 1)."

    Definition 1 supplies only the syntactic notation 'Seq(a1, a2) ≡ a1; a2', while the actual semantic content of each pattern is fixed by the formulas in Table 1. The ΠC algorithm generates Lj by expanding the pattern expression Wj with exactly those Table 1 formulas. Consequently the claimed equivalence between a workflow and its logical specification is true by construction of the workflow semantics, not by an independent equivalence proof against an external UML activity-diagram semantics. The assertion 'equivalent to the processed activity diagram' is therefore a restatement of the definitional mapping rather than a derived result.

full rationale

The strongest formal claim, Claim 8, states that the generated PLTL specification is sound and equivalent to the workflow. In the text this rests on two moves: (i) the soundness theorem is cited from [19], the author's own previous publication, and the feasibility of the whole approach is attributed to [19, 22]; and (ii) the only semantics supplied for the workflow patterns is Table 1 itself, so the 'equivalence' of Wj and Lj is stipulated by the same table that drives the ΠC algorithm. No proof of the soundness theorem, no machine-checked formalization, and no independent benchmark is included in this manuscript, so the central logical result is accepted through a self-citation/definitional chain. This is partial circularity rather than total: the paper's LLM prompts, grammar-based Java/Python skeleton generation, and the worked car-insurance case study are independent content, and the PLTL-to-FOL testing note is an extension idea. The verification assertion Formula (6) is presented without a proof trace, and Claim 3's 'remarkable reliability' has no evaluation; these are evidence gaps, not circular steps. Separately, Table 1 uses undefined symbols a+ and a− and its formulas appear too weak to enforce workflow ordering (e.g., the Seq conjuncts are satisfied by a trace executing a2 before a1); that is a soundness defect worth flagging but it is not itself a circularity. Overall, because the central equivalence claim reduces to the author's own prior work and to the paper's own defining table, the circularity score is 6.

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

The framework rests on hand-chosen pattern sets and logical templates, a soundness proof inherited from the author's prior work, and undefined condition-outcome markers. No new physical or mathematical constants are introduced, but the semantic validity of the patterns is assumed.

free parameters (2)
  • Approved pattern set Π
    The set {Seq, SeqSeq, Cond, Alt, Para, Loop} is chosen by the author as the primitive building blocks; its completeness for arbitrary UML activity diagrams is asserted (Claim 1) but not proven.
  • Fixed logical properties Σ
    The logical formulas in Table 1 are defined by hand for each pattern; their correctness relative to an activity diagram semantics is not derived in this paper.
assumptions (4)
  • domain assumption The ΠC algorithm from Klimek (2019) is sound for all derivable pattern expressions
    The paper cites [19] for soundness of the transformation without reproducing the proof or providing an independent check.
  • domain assumption Activity diagrams for the target systems can be expressed using the six patterns
    Claim 1 asserts coverage; this is not demonstrated beyond the case study.
  • standard math Standard PLTL semantics
    The formulas assume standard propositional linear temporal logic, which is a normal background assumption.
  • ad hoc to paper a1+ and a1- denote positive and negative outcomes of condition a1
    These symbols appear in Table 1 without prior definition or formal semantics.
invented entities (2)
  • a1+ and a1- condition-outcome markers
    purpose: To express the true and false branches of a conditional activity in the logical patterns
    They are introduced in the pattern definitions without a formal semantics that maps them to activity diagram states.
  • Prime variables (e.g., 21')
    purpose: To represent copies of activities from included use case diagrams as fresh atomic propositions
    Technical notation to avoid name clashes when composing activity diagrams; its scope is defined informally.

how reviews work

0 comments
Cite this review

Pith. "Pith review of RE-oriented Model Development with LLM Support and Deduction-based Verification." pith.science (2026). https://pith.science/paper/5SMSB6ZL

@misc{pith2026250608606,
  author       = {Pith},
  title        = {Pith review of: RE-oriented Model Development with LLM Support and Deduction-based Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5SMSB6ZL}},
  note         = {Machine review of arXiv:2506.08606}
}
read the original abstract

The requirements engineering (RE) phase is pivotal in developing high-quality software. Integrating advanced modelling techniques with large language models (LLMs) and formal verification in a logical style can significantly enhance this process. We propose a comprehensive framework that focuses on specific Unified Modelling Language (UML) diagrams for preliminary system development. This framework offers visualisations at various modelling stages and seamlessly integrates large language models and logical reasoning engines. The behavioural models generated with the assistance of LLMs are automatically translated into formal logical specifications. Deductive formal verification ensures that logical requirements and interrelations between software artefacts are thoroughly addressed. Ultimately, the framework facilitates the automatic generation of program skeletons, streamlining the transition from design to implementation.

Figures

Figures reproduced from arXiv: 2506.08606 by the authors.

Figure 4
Figure 4. Architecture f LREd [PITH_FULL_IMAGE:figures/full_fig_p003_4.png] view at source ↗
Figure 2
Figure 2. Use case diagram (top) and tagged scenarios for [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Structured activity diagrams AD2 (top), with AD3 and AD4 (bottom) as call behaviour actions, with initial and final states Definition 1 by the sequential application of the following production rules: 1, 4, 10, 14, 15, 13, 3, 7, 12, 14, 15, 14, 15, 13, 2, 5, 11, 13, 1, 10, 14, 15, 13, 2, 5, 11, 14, 15, 14, 15, 14, 15, 13, 2, 6, 11, 14, 15, 13, 1, 4, 10, 14, 15, 13, 3, 7, 11 [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

34 extracted references · 34 canonical work pages

  1. [19]

    Radosław Klimek. Pattern-based and composition-driven automatic gener- ation of logical specifications for workflow-oriented software models.Jour- nal of Logical and Algebraic Methods in Programming, 104:201–226, 2019

    work page 2019

  2. [1]

    Aho, Monica S

    Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman.Com- pilers: Principles, Techniques, and Tools (2nd Edition). Addison Wesley, 2006

    work page 2006

  3. [2]

    Schneider

    Bowen Alpern and Fred B. Schneider. Defining liveness.Information Pro- cessing Letters, 21 (4):181–185, 1985

    work page 1985

  4. [3]

    Website for ANTLR, 2023

    ANTLR Development Team. Website for ANTLR, 2023. accessed on 17- Apr-2023. 16

    work page 2023

  5. [4]

    Integrating uml activity diagrams with tem- poral logic expressions

    Joao Araujo and Ana Moreira. Integrating uml activity diagrams with tem- poral logic expressions. InProceedings of 10th International Workshop on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD 2005), June 13–14, 2005, Porto, Portugal, pages 477–484, 2005

    work page 2005

  6. [5]

    Autili, P

    M. Autili, P. Inverardi, and P. Pelliccione. Graphical scenarios for speci- fying temporal properties: an automated approach. Automated Software Engineering., 14(3):293–340, sep 2007

    work page 2007

  7. [6]

    Merging of use case models: Semantic foundations

    Stephen Barrett, Daniel Sinnig, Patrice Chalin, and Greg Butler. Merging of use case models: Semantic foundations. In3rd IEEE International Sym- posium on Theoretical Aspects of Software Engineering (TASE’09), pages 182–189, 2009

    work page 2009

  8. [7]

    Berryman and A

    J. Berryman and A. Ziegler.Prompt Engineering for LLMs: The Art and Science of Building Large Language Model–Based Applications. O’Reilly Media, 2024

    work page 2024

Show all 34 references
  1. [8]

    On the role of logic and algebra in software engineering

    Manfred Broy. On the role of logic and algebra in software engineering. In Peter Paule, editor,Mathematics, Computer Science and Logic – A Never Ending Story: The Bruno Buchberger Festschrift, pages 51–68. Springer International Publishing, 2013

    2013

  2. [9]

    Carrillo de Gea, Joaquín Nicolás, José L

    Juan M. Carrillo de Gea, Joaquín Nicolás, José L. Fernández Alemán, Am- brosio Toval, Christof Ebert, and Aurora Vizcaíno. Requirements engineer- ing tools: Capabilities, survey and assessment.Information and Software Technology, 54(10):1142–1157, 2012

    2012

  3. [10]

    Clarke, J.M

    E.M. Clarke, J.M. Wing, and et al. Formal methods: State of the art and future directions. ACM Computing Surveys, 28 (4):626–643, 1996

    1996

  4. [11]

    Temporal and modal logic

    Ernest Allen Emerson. Temporal and modal logic. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995–

  5. [12]

    Angela Fan, Beliz Gokkaya, Mark Harman, Mitya Lyubarskiy, Shubho Sen- gupta, Shin Yoo, and Jie M. Zhang. Large Language Models for Software Engineering: Survey and Open Problems . In2023 IEEE/ACM Interna- tional Conference on Software Engineering: Future of Software Engineer- ...

    2023

  6. [13]

    Gomes, Henry A

    Carla P. Gomes, Henry A. Kautz, Ashish Sabharwal, and Bart Selman. Sat- isfiability solvers. In Frank van Harmelen, Vladimir Lifschitz, and Bruce W. Porter, editors,Handbook of Knowledge Representation, volume 3 ofFoun- dations of Artificial Intelligence, pages 89–134. Elsevier, 2008

    2008

  7. [14]

    The international SAT competitions, web page

    Marijn Heule, Matti Järvisalo, and Martin Suda. The international SAT competitions, web page. http://www.satcompetition.org/, 2022. ac- cessed on 16-May-2022. 17

    2022

  8. [15]

    Hopcroft, Rajeev Motwani, and Jeffrey D

    John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman.Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 2006

    2006

  9. [16]

    Russell R. Hurlbut. A survey of approaches for describing and formalizing use cases. Technical Report XPT-TR-97-03, Expertech, Ltd., 1997

    1997

  10. [17]

    InKreSAT: Modal reasoning via incre- mental reduction to SAT

    Mark Kaminski and Tobias Tebbi. InKreSAT: Modal reasoning via incre- mental reduction to SAT. In Maria Paola Bonacina, editor,24th Inter- national Conference on Automated Deduction (CADE 2013), Lake Placid, New York, 9–14 June 2013, volume 7898 of Lecture Notes in Computer Sci...

    2013

  11. [18]

    Bibliotheca Math- ematica

    Stephen Cole Kleene.Introduction to Metamathematics. Bibliotheca Math- ematica. North-Holland, 1952

    1952

  12. [20]

    Verify- ing data integration agents with deduction-based models

    Radosław Klimek, Łukasz Faber, and Marek Kisiel-Dorohinicki. Verify- ing data integration agents with deduction-based models. InProceedings of Federated Conference on Computer Science and Information Systems (FedCSIS 2013), 8–11 September 2013, Kraków, Poland, pages 1049–1055....

    2013

  13. [21]

    Verification of archimate process spec- ifications based on deductive temporal reasoning

    Radosław Klimek and Piotr Szwed. Verification of archimate process spec- ifications based on deductive temporal reasoning. InProceedings of Fed- erated Conference on Computer Science and Information Systems (FedC- SIS 2013), 8–11 September 2013, Kraków, Poland, pages 1131–1138...

    2013

  14. [22]

    Automatic generation of logical spec- ifications for behavioural models

    Radoslaw Klimek and Julia Witek. Automatic generation of logical spec- ifications for behavioural models. InProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering Workshops, ASEW’24, pages 1–7, New York, NY, USA, 2024. Association for Compu...

    2024

  15. [23]

    Springer-Verlag New York, Inc., 1992

    Zohar Manna and Amir Pnueli.The Temporal Logic of Reactive and Con- current Systems – Specification. Springer-Verlag New York, Inc., 1992

    1992

  16. [24]

    When logic meets engineering: Introduction to logical issues in the history and philosophy of computer science

    Liesbeth De Mol and Giuseppe Primiero. When logic meets engineering: Introduction to logical issues in the history and philosophy of computer science. History and Philosophy of Logic, 36(3):195–204, 2015

    2015

  17. [25]

    John Wiley & Sons, 2003

    Tom Pender.UML Bible. John Wiley & Sons, 2003

    2003

  18. [26]

    The design and implementation of vampire.AI Commun., 15(2,3):91–110, aug 2002

    Alexandre Riazanov and Andrei Voronkov. The design and implementation of vampire.AI Commun., 15(2,3):91–110, aug 2002. 18

    2002

  19. [27]

    Tobias Runge, Ina Schaefer, Loek Cleophas, Thomas Thüm, Der- rick Kourie, and Bruce W. Watson. Tool support for correctness-by- construction. In Reiner Hähnle and Wil van der Aalst, editors,Fundamen- tal Approaches to Software Engineering, pages 25–42, Cham, 2019. Springer Int...

    2019

  20. [28]

    E – a brainiac theorem prover.Journal of AI Communi- cations, 15(2,3):111–126, aug 2002

    Stephan Schulz. E – a brainiac theorem prover.Journal of AI Communi- cations, 15(2,3):111–126, aug 2002

    2002

  21. [29]

    Verified system developmentwiththeautofocustoolchain

    Maria Spichkova, Florian Hölzl, and David Trachtenherz. Verified system developmentwiththeautofocustoolchain. InCésarAndrésandLuisLlana, editors, Proceedings 2nd Workshop on Formal Methods in the Development of Software, WS-FMDS 2012, Paris, France, August 28, 2012, volume 86 ...

    2012

  22. [30]

    The 10th ijcar automated theorem proving system compe- tition – casc-j10.AI Commun., 34(2):163–177, jan 2021

    Geoff Sutcliffe. The 10th ijcar automated theorem proving system compe- tition – casc-j10.AI Commun., 34(2):163–177, jan 2021

    2021

  23. [31]

    Johan van Benthem.Handbook of Logic in Artificial Intelligence and Logic Programming, chapter Temporal Logic, pages 241–350. 4. Clarendon Press, 1993–95

    1993

  24. [32]

    Chi, Quoc V

    Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le, and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models. In Proceedings of the 36th International Conference on Neural Information Processing Sys...

    2022

  25. [33]

    Better algorithms for analyzing and enacting declar- ative workflow languages using LTL

    Michael Westergaard. Better algorithms for analyzing and enacting declar- ative workflow languages using LTL. In Stefanie Rinderle-Ma, Farouk Toumani, and Karsten Wolf, editors,9th International Conference on Busi- ness Process Management (BPM 2011), August 28th – September 2n...

    2011

  26. [34]

    Briand, and Yvan Labiche

    Tao Yue, Lionel C. Briand, and Yvan Labiche. aToucan: An automated framework to derive UML analysis models from use case models. ACM Transactions on Software Engineering and Methodology, 24(3):13:1–13:52, May 2015. 19

    2015

Pith tools

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