Pith. sign in

REVIEW 4 major objections 5 minor 168 references

Working Document -- Formalising Software Requirements with Large Language Models

T0 review · 4 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read This paper presents a structured review of 94 studies on using large language models to formalise natural-language software requirements, and it outlines a research agenda for closing the gap between informal requirements and formally…

desk verdict A self-described working draft that is a useful but unreliable bibliography; the 94-paper corpus is unauditable and the summary tables contain swapped entries, so it should not be cited as a systematic review yet. read the letter →

arxiv 2506.14627 v2 pith:SQPMQOWF submitted 2025-06-17 cs.SE cs.AI

Arshad Beg , Diarmuid O'Donoghue , Rosemary Monahan This is my paper · ORCID
classification cs.SEcs.AI
keywords largelanguagemodelssoftwarerequirementsformalisationformalspecificationstraceabilitystructuredliteraturereviewpromptengineeringchain-of-thoughtreasoningtheoremproving
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

The paper is a working-document survey claiming to summarise ninety-four studies of how large language models help write formal software specifications. It organises the field around two questions: which methodologies translate natural-language requirements into formal notations, and what trends and future directions are emerging. Alongside the core survey, it adds background sections on requirements traceability, formal methods and their tools, and the theoretical frameworks UTP and the Theory of Institutions. The authors intend the review to serve as a map of the area and to motivate a research agenda, called VERIFAI, for combining prompt engineering, chain-of-thought reasoning, and neuro-symbolic verification. If the survey is accurate, it gives newcomers and practitioners a single starting point for understanding what LLM-based formalisation can and cannot do today.

What carries the argument

The load-bearing object is the corpus of 94 selected papers, assembled through keyword searches in five digital libraries and a manual screening pass using explicit inclusion and exclusion criteria. The review machinery consists of the two research questions, RQ1 and RQ2, which organise the synthesis, and the summary tables that condense each paper's tool, framework, and reported results. This structure lets the authors convert a large, heterogeneous literature into a claim about the field's current methodology and its likely next steps, such as the VERIFAI agenda of prompt refinement, chain-of-thought reasoning, and neuro-symbolic verification.

What would settle it

Run the same five-database keyword searches with documented search strings and screening counts, and check whether the 94-paper list is reproduced; if a substantial cluster of relevant 2023–2025 papers on LLM-based formalisation is missing or misclassified, the survey's map of the field would not stand.

Watch

Extended reading notes

Core claim

On its own terms, the paper's central claim is that the field of LLM-based requirements formalisation is real but fragmented: a growing set of tools translate natural language into temporal logics, assertion languages, and program specifications, often with reported accuracies in the 70–95% range, but each tool is a point solution tied to a particular notation or domain. The survey shows that coupling LLMs with verifiers—SMT solvers, bounded model checkers, theorem provers—is a recurring theme, and that verification of the generated artefacts, not just generation, is the persistent open problem. The paper presents the 94-paper corpus as evidence for this picture and derives future directions from it, including iterative refinement, retrieval-augmented prompting, and hybrid neuro-symbolic pipelines.

Load-bearing premise

The load-bearing premise is that the 94 selected papers are representative and accurate enough to support the survey's characterisation of the field and its future-directions claims.

Editorial extensions

If this is right

  • The review implies that LLM-based formalisation is best understood as a collection of domain-specific tools rather than a single general-purpose method.
  • A visible trend across the reviewed papers is coupling LLMs with verifiers such as SMT solvers, model checkers, and theorem provers to check or repair generated specifications.
  • Prompt engineering techniques, including chain-of-thought and retrieval-augmented generation, are presented as promising levers for improving translation accuracy, though the survey notes zero-shot can sometimes outperform few-shot.
  • Verification of LLM output, rather than mere generation, is the open problem that recurs across the corpus and drives the proposed future research directions.

Reading between the lines

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

  • Because the reported accuracies come from different domains and benchmarks, a quantitative cross-study comparison is not yet possible; a standardised benchmark for NL-to-formal translation would turn this survey into a meaningful leaderboard.
  • The inclusion of pre-LLM work such as controlled natural language and ARSENAL suggests that the formalisation problem predates LLMs, so LLM tools could be evaluated against those older baselines as a sanity check for genuine progress.
  • The paper's future-directions section points toward VERIFAI, but the survey itself does not evaluate any single approach; an immediate testable extension would be to run the identified prompting strategies on a fixed set of requirements and compare verified specification rates.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 5 minor

Summary. The manuscript is a working-document literature survey that claims to summarise 94 papers on using large language models (LLMs) to formalise software requirements. It addresses RQ1 by reviewing papers that translate natural-language requirements into formal notations and RQ2 by proposing future directions around prompt engineering, chain-of-thought, retrieval-augmented generation, and neuro-symbolic approaches. It also contains separate sections on requirements traceability, formal methods and tools, UTP, and the Theory of Institutions, followed by appendix tables that summarise the reviewed literature. The paper explicitly identifies itself as a draft and refers readers to two related papers by the same authors for the abstract.

Significance. If the corpus selection and per-paper summaries were accurate and reproducible, this survey would be a useful entry point to a fast-moving area, particularly because it collects industrial case studies and connects LLM-based formalisation to verification tools such as Dafny, VeriFast, and SPIN. The paper is honest about its working-document status and clearly states its research questions. However, the value of the survey is entirely dependent on the trustworthiness and auditability of the summary layer, and the current manuscript contains concrete errors in that layer. The paper does not claim a new empirical result or theory, so its contribution is organisational and descriptive.

major comments (4)
  1. [Section 2 (Methodology for Literature Review)] The selection process for the 94-paper corpus is not reproducible. The section names five databases and the Elicit tool, but it does not provide the exact search strings, the date of each search, the number of records screened, the number excluded at each stage, a PRISMA-style flow diagram, or any inter-rater agreement procedure. With database counts ranging from 17 (IEEE Xplore) to 14,800 (Google Scholar), the step from raw results to the final 94 included papers is unauditable. This matters because the RQ2 future-directions claims in Section 7 are conclusions drawn from that corpus; without a verifiable selection, those conclusions cannot be checked.
  2. [Appendix A, Table 1] Table 1 misassigns the summaries for references [4], [5], and [50]. The body text at the end of Section 3 attributes the SWOT analysis and initial evaluation to [4], the JML comparison between symbolic NLP and ChatGPT to [50], and the domain-model extraction with industrial case studies to [5]. Table 1 instead assigns the SWOT description to [50], the JML comparison to [5], and the domain-model extractor to [4]. Because the paper's central claim is a structured and accurate summary of the literature, these row-level errors directly undermine the reliability of the survey's data layer and must be corrected and checked across all tables.
  3. [Appendix A, Tables 1 and 2] Reference [61] (Laurel) appears twice: once as the last row of Table 1 and again as the first row of Table 2, with identical descriptions. The duplication suggests the tables were assembled without a systematic de-duplication check and raises the question whether other papers are duplicated or omitted. The paper claims 94 papers are summarised, but the appendix tables list only a subset of the references and there is no complete enumeration of the included papers anywhere in the manuscript, so the claimed corpus size cannot be independently verified.
  4. [Abstract and title] The abstract is not self-contained: it instructs the reader to 'refer to abstract of [7,8]' instead of providing an abstract, and the phrase 'nighty-four' instead of 'ninety-four' appears in both the abstract and the introduction. The manuscript also states in its title and opening sentence that it is a working document. These features are acceptable for an arXiv draft but are not appropriate for a journal submission; the abstract must stand alone and the provisional-status language should be removed or clearly qualified if the paper is being submitted for formal publication.
minor comments (5)
  1. [Throughout] There are numerous typographical errors, including 'in-sufficient' in Section 2, 'challange' in Section 3, 'compromising' for 'comprising' in the description of [14], 'sematic' for 'semantic' in the same entry, and 'specifes' in Section 3. A careful proofreading pass is needed.
  2. [Section 4] The traceability section presents a reasonable collection of works, but it does not indicate which of these papers were part of the 94-paper LLM corpus and which are general traceability background. This distinction should be made explicit so the reader can see how the section relates to RQ1 and RQ2.
  3. [Sections 5 and 6] Sections 5 and 6 provide background on formal methods, testing, UTP, and the Theory of Institutions, but their connection to the LLM-focused research questions is not stated. A short paragraph at the start of each section explaining why this background is included and how it supports the survey would improve coherence.
  4. [Appendix tables] The column headers are inconsistent across tables: Tables 1-3 use 'Tool / Framework / Technique', while Tables 4-6 use 'Tool / Framework / Methodology Devised'. In addition, reference [42] appears in two separate rows of Table 5, once for the prompt-engineering review and once for the lost-in-the-middle result; these could be merged or cross-referenced for clarity.
  5. [References] A few references lack complete bibliographic detail, such as [6] and [35], which omit page numbers or DOI information. The reader is also directed to two closely related self-citations [7] and [8] in the abstract; the relationship between this manuscript and those papers should be clarified in the text rather than only through the reference list.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the survey's claims rest on cited external literature, not on the authors' own prior work; self-citations are disclosure, not load-bearing.

full rationale

This paper is a working-document literature survey: its central claims are that it summarises 94 papers on LLM-based formalisation of software requirements and that it organises related material on traceability, formal methods, UTP, and the Theory of Institutions. Those claims are supported by summaries of, and references to, external published work (e.g., nl2spec [17], AssertLLM [23], SpecLLM [54], Laurel [61], SpecGen [57], LeanDojo [93]), not by any derived result whose output equals its input. The only self-citations are [7] and [8], which are prior working documents by the same authors; the abstract explicitly says 'Please refer to abstract of [7,8]' and explains how this draft differs from them. That self-citation is disclosed and descriptive; it is not used as evidence for the survey's factual claims, nor does it supply a premise from which the survey's conclusions are forced. There is no fitted parameter renamed as a prediction, no equation that reduces to a definition by construction, and no uniqueness theorem imported from the authors' prior work. The selection methodology is admittedly incomplete (no search strings, no screening counts, no PRISMA flow diagram), and the appendix contains apparent row-swapping and duplication errors (e.g., Table 1 swaps the descriptions for [4], [5], and [50]; Table 2 repeats [61]). Those are correctness and reproducibility concerns, not circularity: an unauditable corpus could weaken the survey's conclusions, but it does not make those conclusions equivalent to their own inputs. Accordingly, the appropriate finding is no significant circularity, score 0.

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

The paper introduces no free parameters and no invented entities. Its only axioms are the representativeness of the selected corpus and the trustworthiness of transcribed results from the 94 surveyed papers, both of which are standard assumptions for a literature review but are not audited here.

assumptions (2)
  • domain assumption The 94-paper corpus, identified via keyword searches and Elicit, adequately represents the research landscape of LLM-based software requirements formalisation.
    The survey's conclusions and future-directions section depend on the assumption that the selection is representative. The methodology in Section 2 lists databases and Elicit but provides no screening counts or search strings.
  • domain assumption The reported accuracy figures and performance claims from the surveyed papers can be taken at face value.
    The survey transcribes numbers such as 94.4% accuracy, 99.7% recall, and 71% formalisation success without independent verification. All reported metrics are attributed to the original papers.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Working Document -- Formalising Software Requirements with Large Language Models." pith.science (2026). https://pith.science/paper/SQPMQOWF

@misc{pith2026250614627,
  author       = {Pith},
  title        = {Pith review of: Working Document -- Formalising Software Requirements with Large Language Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SQPMQOWF}},
  note         = {Machine review of arXiv:2506.14627}
}
read the original abstract

This draft is a working document, having a summary of nighty-four (94) papers with additional sections on Traceability of Software Requirements (Section 4), Formal Methods and Its Tools (Section 5), Unifying Theories of Programming (UTP) and Theory of Institutions (Section 6). Please refer to abstract of [7,8]. Key difference of this draft from our recently anticipated ones with similar titles, i.e. AACS 2025 [7] and SAIV 2025 [8] is: [7] is a two page submission to ADAPT Annual Conference, Ireland. Submitted on 18th of March, 2025, it went through the light-weight blind review and accepted for poster presentation. Conference was held on 15th of May, 2025; [8] is a nine page paper with additional nine pages of references and summary tables, submitted to Symposium on AI Verification (SAIV 2025) on 24th of April, 2025. It went through rigorous review process. The uploaded version on arXiv.org [8] is the improved one of the submission, after addressing the specific suggestions to improve the paper.

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

168 extracted references · 23 canonical work pages

  1. [4]

    Chetan Arora, John Grundy, and Mohamed Abdelrazek. 2023. Advancing Requirements Engineering through Generative AI: Assessing the Role of LLMs. (2023). arXiv:cs.SE/2310.13976 https://arxiv.org/abs/2310.13976

    arXiv 2023

  2. [5]

    Chetan Arora, Mehrdad Sabetzadeh, Lionel Briand, and Frank Zimmer. 2016. Extracting domain models from natural-language requirements: approach and industrial evaluation. In Proceedings of the ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems (MODELS ’16). Association for Computing Machinery, New York, NY, USA, 250–26...

    arXiv 2016

  3. [50]

    Iat Tou Leong and Raul Barbosa. 2023. Translating Natural Language Requirements to Formal Specifications: A Study on GPT and Symbolic NLP. In 2023 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W) . 259–262. https://doi.org/10.1109/DSN- W58399.2023.00065

    arXiv 2023

  4. [61]

    Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, and Yuanyuan Zhou. 2024. Laurel: Generating Dafny Assertions Using Large Language Models. (2024). arXiv:cs.LO/2405.16792 https://arxiv.org/abs/2405.16792

    arXiv 2024

  5. [1]

    Gul Agha and Karl Palmskog. 2018. A survey of statistical model checking. ACM Transactions on Modeling and Computer Simulation 28, 1 (2018), 6:1–6:39. https://doi.org/10.1145/3158668

    doi:10.1145/3158668 2018

  6. [2]

    Nasir Ali, Yann-Gaël Guéhéneuc, and Giuliano Antoniol. 2013. Trustrace: Mining Software Repositories to Improve the Accuracy of Requirement Traceability Links. IEEE Transactions on Software Engineering 39, 5 (2013), 725–741. https://doi.org/10.1109/TSE.2012.71

    work page doi:10.1109/tse.2012.71 2013

  7. [3]

    Xavier Amatriain. 2024. Prompt Design and Engineering: Introduction and Advanced Methods. (2024). arXiv:cs.SE/2401.14423 https://arxiv.org/abs/ 2401.14423

    arXiv 2024

  8. [6]

    Erika Asnina, Bernards Gulbis, Janis Osis, Gundars Alksnis, Uldis Donins, and Armands Slihte. 2011. Backward Requirements Traceability within the Topology-based Model Driven Software Development. In MDA & MDSD 2011 - Proceedings of the 3rd International Workshop on Model-Driven Architecture and Modeling-Driven Software Development, In conjunction with ENA...

    2011

Show all 168 references
  1. [7]

    Arshad Beg, Diarmuid O’Donoghue, and Rosemary Monahan. 2025. Formalising Software Requirements using Large Language Models. (2025). arXiv:cs.SE/2506.10704 https://arxiv.org/abs/2506.10704

    2025 arXiv

  2. [8]

    Arshad Beg, Diarmuid O’Donoghue, and Rosemary Monahan. 2025. A Short Survey on Formalising Software Requirements using Large Language Models. (2025). arXiv:cs.SE/2506.11874 https://arxiv.org/abs/2506.11874

    2025 arXiv

  3. [9]

    Ron Bell. 2006. Introduction to IEC 61508. In Proceedings of the 10th Australian Workshop on Safety Critical Systems and Software - Volume 55 (SCS ’05). Australian Computer Society, Inc., AUS, 3–12

    2006

  4. [10]

    Maciej Besta, Florim Memedi, Zhenyu Zhang, Robert Gerstenberger, Nils Blach, Piotr Nyczyk, Marcin Copik, Grzegorz Kwasniewski, Jürgen Müller, Lukas Gianinazzi, Ales Kubicek, Hubert Niewiadomski, Onur Mutlu, and Torsten Hoefler. 2024. Topologies of Reasoning: Demystifying Chain...

    2024 doi

  5. [11]

    Benjamin Brosgol. 2011. Do-178c: the next avionics safety standard. Ada Lett. 31, 3 (Nov. 2011), 5–6. https://doi.org/10.1145/2070336.2070341

    2011

  6. [12]

    Andrew Butterfield and Frédéric Tuong. 2023. Applying Formal Verification to an Open-Source Real-Time Operating System. In Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday (Lecture Notes in Computer Science) , Jona...

    2023 doi

  7. [13]

    Kelleher, Shen Fei, Gui Tong, Jiandong Ding, and Puchao Zhang

    Bora Caglayan, Mingxue Wang, John D. Kelleher, Shen Fei, Gui Tong, Jiandong Ding, and Puchao Zhang. 2024. BIS: NL2SQL Service Evaluation Benchmark for Business Intelligence Scenarios. In Service-Oriented Computing: 22nd International Conference, ICSOC 2024, Tunis, Tunisia, Dec...

    2024 doi

  8. [14]

    Daggitt, Omri Isac, Guy Katz, Verena Rieser, and Oliver Lemon

    Marco Casadio, Tanvi Dinkar, Ekaterina Komendantskaya, Luca Arnaboldi, Matthew L. Daggitt, Omri Isac, Guy Katz, Verena Rieser, and Oliver Lemon

  9. [15]

    Farid Cerbah and Jérôme Euzenat. 2001. Using Terminology Extraction to Improve Traceability from Formal Models to Textual Requirements. In Natural Language Processing and Information Systems, Mokrane Bouzeghoub, Zoubida Kedad, and Elisabeth Métais (Eds.). Springer Berlin Heide...

    2001

  10. [16]

    Cleland-Huang, C.K

    J. Cleland-Huang, C.K. Chang, and M. Christensen. 2003. Event-based traceability for managing evolutionary change. IEEE Transactions on Software Engineering 29, 9 (2003), 796–810. https://doi.org/10.1109/TSE.2003.1232285

    2003 arXiv

  11. [17]

    Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. 2023. nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models. (2023). arXiv:cs.LO/2303.04864 https://arxiv.org/abs/2303.04864

    2023 arXiv

  12. [18]

    Juan Ortiz Couder, Dawson Gomez, and Omar Ochoa. 2024. Requirements Verification Through the Analysis of Source Code by Large Language Models. In SoutheastCon 2024. 75–80. https://doi.org/10.1109/SoutheastCon52093.2024.10500073

    2024

  13. [19]

    Ana Marcia Debiasi Duarte, Denio Duarte, and Marcello Thiry. 2016. TraceBoK: Toward a Software Requirements Traceability Body of Knowledge. In 2016 IEEE 24th International Requirements Engineering Conference (RE) . 236–245. https://doi.org/10.1109/RE.2016.32

    2016 doi

  14. [20]

    Elicit. 2025. Elicit - The AI Research Assistant. https://elicit.com. (2025). Accessed: 2025-04-11 at 12:49PM

    2025

  15. [21]

    Michael D. Ernst. 2017. Natural Language is a Programming Language: Applying Natural Language Processing to Software Development. In 2nd Summit on Advances in Programming Languages (SNAPL 2017) (Leibniz International Proceedings in Informatics (LIPIcs)) , Benjamin S. Lerner, R...

    2017 doi

  16. [22]

    Wen Fan, Marilyn Rego, Xin Hu, Sanya Dod, Zhaorui Ni, Danning Xie, Jenna DiVincenzo, and Lin Tan. 2025. Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast. (2025). arXiv:cs.SE/2411.02318 https://arxiv.org/abs/2411.02318

    2025 arXiv

  17. [23]

    Wenji Fang, Mengming Li, Min Li, Zhiyuan Yan, Shang Liu, Hongce Zhang, and Zhiyao Xie. 2024. AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs. In 2024 IEEE LLM Aided Design Workshop (LAD) . 1–1. https://doi.org/10.1109/LAD62341.2...

    2024

  18. [24]

    Mohamad Fazelnia, Mehdi Mirakhorli, and Hamid Bagheri. 2024. Translation Titans, Reasoning Challenges: Satisfiability-Aided Language Models for Detecting Conflicting Requirements. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (A...

    2024

  19. [25]

    Antonio Filieri, Carlo Ghezzi, and Giordano Tamburrelli. 2011. Run-time efficient probabilistic model checking. In Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011 , Richard N. Taylor, Harald C. Gall, and Nenad Medvidovic (Eds.). ACM, 341–350...

    2011

  20. [26]

    Simon Foster, James Baxter, Ana Cavalcanti, Jim Woodcock, and Frank Zeyda. 2020. Unifying semantic foundations for automated verification tools in Isabelle/UTP. Science of Computer Programming 197 (2020), 102510. https://doi.org/10.1016/j.scico.2020.102510

    2020

  21. [27]

    Saurabh Gadia, Cyrille Artho, and Gedare Bloom. 2016. Verifying Nested Lock Priority Inheritance in RTEMS with Java Pathfinder. In Formal Methods and Software Engineering , Kazuhiro Ogata, Mark Lawford, and Shaoying Liu (Eds.). Springer International Publishing, Cham, 417–432....

    2016 doi

  22. [28]

    Marie-Claude Gaudel. 1995. Testing can be formal, too. In TAPSOFT‘95: Theory and Practice of Software Development, 6th International Joint Conference CAAP/FASE (Lecture Notes in Computer Science) , Peter D. Mosses, Mogens Nielsen, and Michael I. Schwartzbach (Eds.), Vol. 915. ...

    1995 doi

  23. [29]

    E. C. Genvigir and N. L. Vijaykumar. 2010. Requirements Traceability. In Handbook of Research on Software Engineering and Productivity Technologies: Implications of Globalization , Muthu Ramachandran and Ricardo de Carvalho (Eds.). IGI Global Scientific Publishing, 102–120. ht...

    2010 doi

  24. [30]

    Vincenzo Gervasi and Bashar Nuseibeh. 2002. Lightweight validation of natural language requirements. Softw. Pract. Exper. 32, 2 (Feb. 2002), 113–133. https://doi.org/10.1002/spe.430

    2002 doi

  25. [31]

    Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar, and Wilfried Steiner. 2016. ARSENAL: Automatic Requirements Specification Extraction from Natural Language. In NASA Formal Methods, Sanjai Rayadurgam and Oksana Tkachuk (Eds.). Springer Internationa...

    2016

  26. [32]

    Goguen and Rod M

    Joseph A. Goguen and Rod M. Burstall. 1992. Institutions: abstract model theory for specification and programming. J. ACM 39, 1 (Jan. 1992), 95–146. https://doi.org/10.1145/147508.147524

    1992

  27. [33]

    Arda Goknil, Ivan Kurtev, Klaas van den Berg, and Jan-Willem Veldhuis. 2011. Semantics of trace relations in requirements models for consistency checking and inferencing. Software & Systems Modeling 10, 1 (2011), 31–54. https://doi.org/10.1007/s10270-009-0142-3

    2011 doi

  28. [34]

    George Granberry, Wolfgang Ahrendt, and Moa Johansson. 2025. Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods. In Integrated Formal Methods, Nikolai Kosmatov and Laura Kovács (Eds.). Springer Nature Switzerland, Cham, 307–325

    2025

  29. [35]

    George Granberry, Wolfgang Ahrendt, and Moa Johansson. 2025. Towards Integrating Copiloting and Formal Methods. InLeveraging Applications of Formal Methods, Verification and Validation. Specification and Verification, Tiziana Margaria and Bernhard Steffen (Eds.). Springer Natu...

    2025

  30. [36]

    Greenspan, Alexander Borgida, and John Mylopoulos

    Sol J. Greenspan, Alexander Borgida, and John Mylopoulos. 1986. A requirements modeling language and its logic. Information Systems 11, 1 (1986), 9–23. https://doi.org/10.1016/0306-4379(86)90020-7

    1986 doi

  31. [37]

    Jin Guo, Jinghui Cheng, and Jane Cleland-Huang. 2017. Semantically enhanced software traceability using deep learning techniques. In Proceedings of the 39th International Conference on Software Engineering (ICSE ’17) . IEEE Press, 3–14. https://doi.org/10.1109/ICSE.2017.9

    2017 doi

  32. [38]

    Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner

    Christopher Hahn, Frederik Schmitt, Julia J. Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner. 2022. Formal Specifications from Natural Language. (2022). arXiv:cs.SE/2206.01962 https://arxiv.org/abs/2206.01962

    2022 arXiv

  33. [39]

    Jones, and Kristin Y

    Abigail Hammer, Matthew Cauwels, Benjamin Hertz, Phillip H. Jones, and Kristin Y. Rozier. 2022. Integrating runtime verification into an automated UAS traffic management system. Innov. Syst. Softw. Eng. 18, 4 (2022), 567–580. https://doi.org/10.1007/S11334-021-00407-5

    2022 doi

  34. [40]

    Ashlee Holbrook, Sravanthi Vadlamudi, and Alain April

    Jane Huffman Hayes, Alex Dekhtyar, Senthil Karthikeyan Sundaram, E. Ashlee Holbrook, Sravanthi Vadlamudi, and Alain April. 2007. REquirements TRacing On target (RETRO): improving software maintenance through traceability recovery. Innovations in Systems and Software Engineerin...

    2007 doi

  35. [41]

    Hierons, Kirill Bogdanov, Jonathan P

    Robert M. Hierons, Kirill Bogdanov, Jonathan P. Bowen, Rance Cleaveland, John Derrick, Jeremy Dick, Marian Gheorghe, Mark Harman, Kalpesh Kapoor, Paul J. Krause, Gerald Lüttgen, Anthony J. H. Simons, Sergiy A. Vilkomir, Martin R. Woodward, and Hussein Zedan. 2009. Using formal...

    2009

  36. [42]

    Le, Abhishek Kumar, James R

    Cheng-Yu Hsieh, Yung-Sung Chuang, Chun-Liang Li, Zifeng Wang, Long T. Le, Abhishek Kumar, James R. Glass, Alexander Ratner, Chen-Yu Lee, Ranjay Krishna, and Tomas Pfister. 2024. Found in the middle: Calibrating Positional Attention Bias Improves Long Context Utilization. In Fi...

    2024

  37. [43]

    Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen

    Edward J. Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. 2022. LoRA: Low-Rank Adaptation of Large Language Models. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 20...

    2022

  38. [44]

    Marieke Huisman, Dilian Gurov, and Alexander Malkis. 2024. Formal Methods: From Academia to Industrial Practice. A Travel Guide. (2024). arXiv:cs.SE/2002.07279 https://arxiv.org/abs/2002.07279

    2024 arXiv

  39. [45]

    Thomas Hérault, Richard Lassaigne, Frédéric Magniette, and Sylvain Peyronnet. 2004. Approximate probabilistic model checking. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004 (Lecture Notes in Computer Science) , Bernhard S...

    2004 doi

  40. [46]

    Padma Iyenghar, Elke Pulvermueller, and Clemens Westerkamp. 2011. Towards Model-Based Test automation for embedded systems using UML and UTP. In ETFA2011. 1–9. https://doi.org/10.1109/ETFA.2011.6058982

    2011

  41. [47]

    Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Mił oś, Yuhuai Wu, and Mateja Jamnik. 2022. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In Advances in Neural Information Processing Systems , ...

    2022

  42. [48]

    Takeshi Kojima, Shixiang (Shane) Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. 2022. Large Language Models are Zero-Shot Reasoners. In Advances in Neural Information Processing Systems , S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh (Eds.), Vol. 35. C...

    2022

  43. [49]

    Kwiatkowska, Gethin Norman, and David Parker

    Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2002. PRISM: probabilistic symbolic model checker. In Computer Performance Evaluation, Modelling Techniques and Tools, 12th International Conference, TOOLS 2002 (Lecture Notes in Computer Science) , Tony Field, Peter G. Ha...

    2002 doi

  44. [51]

    Henrik Leopold, Jan Mendling, and Artem Polyvyanyy. 2014. Supporting Process Model Validation through Natural Language Generation. IEEE Transactions on Software Engineering 40, 8 (2014), 818–840. https://doi.org/10.1109/TSE.2014.2327044

    2014

  45. [52]

    Patrick Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich Küttler, Mike Lewis, Wen-tau Yih, Tim Rocktäschel, Sebastian Riedel, and Douwe Kiela. 2020. Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks. In Advances in ...

    2020

  46. [53]

    Jia Li, Ge Li, Yongmin Li, and Zhi Jin. 2025. Structured Chain-of-Thought Prompting for Code Generation. ACM Trans. Softw. Eng. Methodol. 34, 2, Article 37 (Jan. 2025), 23 pages. https://doi.org/10.1145/3690635

    2025 doi

  47. [54]

    Mengming Li, Wenji Fang, Qijun Zhang, and Zhiyao Xie. 2024. SpecLLM: Exploring Generation and Review of VLSI Design Specification with Large Language Model. (2024). arXiv:cs.AR/2401.13266 https://arxiv.org/abs/2401.13266

    2024 arXiv

  48. [55]

    Yunshui Li, Binyuan Hui, Xiaobo Xia, Jiaxi Yang, Min Yang, Lei Zhang, Shuzheng Si, Ling-Hao Chen, Junhao Liu, Tongliang Liu, Fei Huang, and Yongbin Li. 2024. One-Shot Learning as Instruction Data Prospector for Large Language Models. (2024). arXiv:cs.CL/2312.10302 https: //arx...

    2024 arXiv

  49. [56]

    Dennis, Clare Dixon, and Michael Fisher

    Matt Luckcuck, Marie Farrell, Louise A. Dennis, Clare Dixon, and Michael Fisher. 2019. Formal Specification and Verification of Autonomous Robotic Systems: A Survey. ACM Comput. Surv. 52, 5, Article 100 (Sept. 2019), 41 pages. https://doi.org/10.1145/3342355

    2019 doi

  50. [57]

    Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2024. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. (2024). arXiv:cs.SE/2401.08807 https://arxiv.org/abs/2401.08807

    2024 arXiv

  51. [58]

    Abdulkadir Ahmad Madaki and Wan Mohd Nazmee Wan Zainon. 2022. A Review on Tools and Techniques for Visualizing Software Requirement Traceability. In Proceedings of the 11th International Conference on Robotics, Vision, Signal Processing and Power Applications , Nor Muzlifah Ma...

    2022

  52. [59]

    Shantanu Mandal, Adhrik Chethan, Vahid Janfaza, S M Farabi Mahmud, Todd A Anderson, Javier Turek, Jesmin Jahan Tithi, and Abdullah Muzahid

  53. [60]

    Lopes, Iris Ma, and James Noble

    Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. 2024. Towards AI-Assisted Synthesis of Verified Dafny Methods. Proc. ACM Softw. Eng. 1, FSE, Article 37 (July 2024), 24 pages. https://doi.org/10.1145/3643763

    2024 doi

  54. [62]

    Prasita Mukherjee and Benjamin Delaware. 2024. Towards Automated Verification of LLM-Synthesized C Programs. (2024). arXiv:cs.PL/2410.14835 https://arxiv.org/abs/2410.14835

    2024

  55. [63]

    Anmol Nayak, Hari Prasad Timmapathini, Vidhya Murali, Karthikeyan Ponnalagu, Vijendran Gopalan Venkoparao, and Amalinda Post. 2022. Req2Spec: Transforming Software Requirements into Formal Specifications Using Natural Language Processing. In Requirements Engineering: Foundatio...

    2022

  56. [64]

    Erika Nazaruka and J?nis Osis. 2018. Determination of Natural Language Processing Tasks and Tools for Topological Functioning Modelling. In Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2018) . SCITEPRESS - Sc...

    2018 doi

  57. [65]

    Sabina-Cristiana Necula, Florin Dumitriu, and Valerică Greavu-S, erban. 2024. A Systematic Literature Review on Using Natural Language Processing in Software Requirements Engineering. Electronics 13, 11 (2024). https://doi.org/10.3390/electronics13112055

    2024 doi

  58. [66]

    Rani Nelken and Nissim Francez. 1996. Automatic translation of natural language system specifications into temporal logic. In Computer Aided Verification, Rajeev Alur and Thomas A. Henzinger (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 360–371. Working Document - Fo...

    1996

  59. [67]

    Ali Nouri, Beatriz Cabrero-Daniel, Fredrik Törner, Håkan Sivencrona, and Christian Berger. 2024. Engineering Safety Requirements for Autonomous Driving with Large Language Models. In 2024 IEEE 32nd International Requirements Engineering Conference (RE) . 218–228. https://doi.o...

    2024

  60. [68]

    Wiktor Nowakowski, Michał Śmiałek, Albert Ambroziewicz, and Tomasz Straszak. 2013. Requirements-level language and tools for capturing software system essence. Computer Science and Information Systems 10, 4 (2013), 1499–1524

    2013

  61. [69]

    Osborne and C.K

    M. Osborne and C.K. MacNish. 1996. Processing natural language software requirement specifications. In Proceedings of the Second International Conference on Requirements Engineering . 229–236. https://doi.org/10.1109/ICRE.1996.491451

    1996

  62. [70]

    Rob Palin, David Ward, Ibrahim Habli, and Roger Rivett. 2011. ISO 26262 safety cases: Compliance and assurance. In6th IET International Conference on System Safety 2011 . 1–6. https://doi.org/10.1049/cp.2011.0251

    2011

  63. [71]

    Pinheiro and J.A

    F.A.C. Pinheiro and J.A. Goguen. 1996. An object-oriented tool for tracing requirements. In Proceedings of the Second International Conference on Requirements Engineering. 219–. https://doi.org/10.1109/ICRE.1996.491449

    1996

  64. [72]

    Anamaria-Roberta Preda, Christoph Mayr-Dorn, Atif Mashkoor, and Alexander Egyed. 2024. Supporting High-Level to Low-Level Requirements Coverage Reviewing with Large Language Models. In Proceedings of the 21st International Conference on Mining Software Repositories (MSR ’24) ....

    2024

  65. [73]

    Dennis, and André Freitas

    Xin Quan, Marco Valentino, Louise A. Dennis, and André Freitas. 2024. Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving. (2024). arXiv:cs.CL/2405.01379 https://arxiv.org/abs/2405.01379

    2024 arXiv

  66. [74]

    Reinpold, Marvin Schieseck, Lukas P

    Lasse M. Reinpold, Marvin Schieseck, Lukas P. Wagner, Felix Gehlhoff, and Alexander Fay. 2024. Exploring LLMs for Verifying Technical System Specifications Against Requirements. (2024). arXiv:cs.SE/2411.11582 https://arxiv.org/abs/2411.11582

    2024 arXiv

  67. [75]

    Patrick Rempel and Parick Mäder. 2017. Preventing Defects: The Impact of Requirements Traceability Completeness on Software Quality. IEEE Transactions on Software Engineering 43, 8 (2017), 777–797. https://doi.org/10.1109/TSE.2016.2622264

    2017

  68. [76]

    A.M. Salem. 2006. Improving Software Quality through Requirements Traceability Models. In IEEE International Conference on Computer Systems and Applications, 2006. 1159–1162. https://doi.org/10.1109/AICCSA.2006.205236

    2006

  69. [77]

    Ahmed M Salem. 2010. Model for Enhancing Requirements Traceability and Analysis. International Journal of Advanced Computer Science and Applications 1, 5 (2010). https://doi.org/10.14569/IJACSA.2010.010503

    2010 arXiv

  70. [78]

    Sabnam Sengupta, Ananya Kanjilal, and Swapan Bhattacharya. 2008. Requirement Traceability in Software Development Process: An Empirical Approach. In 2008 The 19th IEEE/IFIP International Symposium on Rapid System Prototyping . 105–111. https://doi.org/10.1109/RSP.2008.14

    2008 doi

  71. [79]

    Kashun Shum, Shizhe Diao, and Tong Zhang. 2023. Automatic Prompt Augmentation and Selection with Chain-of-Thought from Labeled Data. In Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023 , Houda Bouamor, Juan Pino, and Kalika ...

    2023 doi

  72. [80]

    Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, and Le Song. 2020. Code2Inv: A Deep Learning Framework for Program Verification. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham, 151–164

    2020

  73. [81]

    Cordeiro

    Norbert Tihanyi, Ridhi Jain, Yiannis Charalambous, Mohamed Amine Ferrag, Youcheng Sun, and Lucas C. Cordeiro. 2024. A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification. (2024). arXiv:cs.SE/2305.14752 https: //arxiv.or...

    2024 arXiv

  74. [82]

    RICHARD TORKAR, TONY GORSCHEK, ROBERT FELDT, MIKAEL SVAHNBERG, UZAIR AKBAR RAJA, and KASHIF KAMRAN. 2012. REQUIRE- MENTS TRACEABILITY: A SYSTEMATIC REVIEW AND INDUSTRY CASE STUDY. International Journal of Software Engineering and Knowledge Engineering 22, 03 (2012), 385–433. h...

    2012 doi

  75. [83]

    Boshi Wang, Xiang Deng, and Huan Sun. 2022. Iteratively Prompt Pre-trained Language Models for Chain of Thought. In Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing , Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang (Eds.). Association for ...

    2022 doi

  76. [84]

    Bangchao Wang, Rong Peng, Zhuo Wang, Xiaomin Wang, and Yuanbang Li. 2020. An Automated Hybrid Approach for Generating Requirements Trace Links. International Journal of Software Engineering and Knowledge Engineering 30, 07 (2020), 1005–1048. https://doi.org/10.1142/S0218194020...

    2020 doi

  77. [85]

    Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed Chi, Quoc V Le, and Denny Zhou. 2022. Chain-of-Thought Prompting Elicits Reasoning in Large Language Models. In Advances in Neural Information Processing Systems , S. Koyejo, S. Mohamed, A. Agarw...

    2022

  78. [86]

    Jules White, Quchen Fu, Sam Hays, Michael Sandborn, Carlos Olea, Henry Gilbert, Ashraf Elnashar, Jesse Spencer-Smith, and Douglas C. Schmidt. 2023. A Prompt Pattern Catalog to Enhance Prompt Engineering with ChatGPT. CoRR abs/2302.11382 (2023). https://doi.org/10.48550/ARXIV.2...

    2023 doi arXiv

  79. [87]

    Jim Woodcock and Ana Cavalcanti. 2002. The Semantics of Circus. In ZB 2002: Formal Specification and Development in Z and B , Didier Bert, Jonathan P. Bowen, Martin C. Henson, and Ken Robinson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 184–203. https://doi.org/10....

    2002 doi

  80. [88]

    Jim Woodcock and Ana Cavalcanti. 2004. A Tutorial Introduction to Designs in Unifying Theories of Programming. In Integrated Formal Methods, Eerke A. Boiten, John Derrick, and Graeme Smith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 40–66

    2004

  81. [89]

    Haoze Wu, Clark Barrett, and Nina Narodytska. 2024. Lemur: Integrating Large Language Models in Automated Program Verification. (2024). arXiv:cs.FL/2310.04870 https://arxiv.org/abs/2310.04870 16 Arshad Beg, Diarmuid O’Donoghue, and Rosemary Monahan

    2024 arXiv

  82. [90]

    Weijia Xu, Andrzej Banburski-Fahey, and Nebojsa Jojic. 2023. Reprompting: Automated Chain-of-Thought Prompt Inference Through Gibbs Sampling. CoRR abs/2305.09993 (2023). https://doi.org/10.48550/ARXIV.2305.09993 arXiv:2305.09993

    2023 doi arXiv

  83. [91]

    Yilongfei Xu, Jincao Feng, and Weikai Miao. 2024. Learning from Failures: Translation of Natural Language Requirements into Linear Temporal Logic with Large Language Models. In 2024 IEEE 24th International Conference on Software Quality, Reliability and Security (QRS) . 204–21...

    2024

  84. [92]

    Rongjie Yan, Chih-Hong Cheng, and Yesheng Chai. 2015. Formal consistency checking over specifications in natural languages. In 2015 Design, Automation & Test in Europe Conference & Exhibition (DATE) . 1677–1682

    2015

  85. [93]

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2023. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. InAdvances in Neural Information Processing Systems , A. Oh, T. Naumann...

    2023

  86. [94]

    Junyi Yao, Yijiang Liu, Zhen Dong, Mingfei Guo, Helan Hu, Kurt Keutzer, Li Du, Daquan Zhou, and Shanghang Zhang. 2024. PromptCoT: Align Prompt Distribution via Adapted Chain-of-Thought. In 2024 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR) . 7027–7037. ...

    2024

  87. [95]

    Xi Ye and Greg Durrett. 2022. The Unreliability of Explanations in Few-shot Prompting for Textual Reasoning. In Advances in Neural Information Processing Systems, S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh (Eds.), Vol. 35. Curran Associates, Inc., 30378–30392

    2022

  88. [96]

    Haodi Zhang, Min Cai, Xinhe Zhang, Chen Jason Zhang, Rui Mao, and Kaishun Wu. 2023. Self-Convinced Prompting: Few-Shot Question Answering with Repeated Introspection. (2023). arXiv:cs.CL/2310.05035 https://arxiv.org/abs/2310.05035 Working Document - Formalising Software Requir...

    2023 arXiv

  89. [99]

    LLM-based Code Verifica- tion Uses LLMs like GPT-3.5 to verify code by analyzing requirements and explaining whether they are met

  90. [100]

    nl2spec A framework leveraging LLMs to generate formal specifications from natural language, addressing ambiguity in system requirements with iterative refinement

  91. [101]

    Explanation-Refiner A neuro-symbolic framework integrating LLMs and theorem provers to formalize and validate explanatory sentences, providing error correction and feedback for improving NLI models

  92. [102]

    Not Specified Analyzes research directions in software requirement engineering, con- ducting a SWOT analysis and sharing evaluation findings

  93. [103]

    ChatGPT Compares the performance of symbolic NLP and ChatGPT in generating correct JML output from natural language preconditions

    Symbolic NLP vs. ChatGPT Compares the performance of symbolic NLP and ChatGPT in generating correct JML output from natural language preconditions

  94. [104]

    Domain Model Extractor Generates domain models from natural language requirements in an industrial case study, evaluating accuracy and performance

  95. [105]

    SpecSyn A framework using LLMs for automatic synthesis of software specifica- tions, improving accuracy by 21% over previous tools

  96. [106]

    AssertLLM A tool generating assertions for hardware verification from design specifications using three customized LLMs, achieving 89% correctness

  97. [107]

    Formal Verification of NASA’s Software Reports on formal verification of NASA’s Node Control Software natural language specifications, highlighting errors and lessons learned

  98. [108]

    SpecLLM Explores using LLMs for generating and reviewing VLSI design specifi- cations, improving chip design documentation

  99. [109]

    Requirements Specification Language (RSL), ReDSeeDS Enhanced software requirements specification using constrained natu- ral language and automated transformations into code

  100. [110]

    ARSENAL Framework and Methodology Automated extraction of requirements specification from natural lan- guage with automatic verification

  101. [111]

    BPM-to-NL Translation Process Generated natural language descriptions from business process models for better validation

  102. [112]

    Summary of LLMs related literature: Tools, Frameworks, and Achievements 18 Arshad Beg, Diarmuid O’Donoghue, and Rosemary Monahan Paper Tool / Framework / Tech- nique Description

    Laurel A framework to generate Dafny assertions to automate program verifi- cation process for a SMT solver Table 1. Summary of LLMs related literature: Tools, Frameworks, and Achievements 18 Arshad Beg, Diarmuid O’Donoghue, and Rosemary Monahan Paper Tool / Framework / Tech- ...

  103. [113]

    Laurel A framework to generate Dafny assertions to automate program verifi- cation process for a SMT solver

  104. [114]

    Controlled Natural Lan- guage (CL) with ANLT Expressed software requirements in a limited set of natural language and translated to logical expressions to detect ambiguities

  105. [115]

    LLM-based Analysis for Smart Grid Requirements Improved smart grid requirement specifications with GPT-4o and Claude 3.5 Sonnet, achieving F1-scores between 79% - 94%

  106. [116]

    NL-to-LTL Translation via LLMs Converted unstructured natural language requirements to NL-LTL pairs, achieving 94.4% accuracy on public datasets

  107. [117]

    ESBMC-AI Combined LLMs with Formal Verification to detect and fix software vulnerabilities with high accuracy

  108. [118]

    LLM-based Formal Specifi- cations Translation Translated natural language into formal rules (regex, FOL, LTL) with high adaptability and performance

  109. [119]

    SynVer Framework Synthesized and verified C programs using the Verified Software Toolchain

  110. [120]

    LLM-based Requirement Coverage Analysis Ensured low-level software requirements met high-level requirements, achieving 99.7% recall in spotting missing coverage

  111. [121]

    SAT-LLM Integrated SMT solvers with LLMs to improve conflict identification in requirements; significantly outperformed standalone LLMs in detecting complex conflicts

  112. [122]

    NLP for Software Develop- ment Assessed NLP techniques for various software development stages, highlighting their suitability for generating assertions and processing developer queries

  113. [123]

    Req2Spec NLP-based tool that formalises natural language requirements for HAN- FOR; achieved 71% accuracy in formalising 222 automotive require- ments at BOSCH

  114. [124]

    RML (Requirements Model- ing Language) Introduced a conceptual model-based framework ensuring precision, consistency, and clarity in requirements writing

  115. [125]

    GPT-4o for VeriFast Verifi- cation Evaluated GPT-4o’s ability to generate C program specifications for VeriFast; found that while functional behavior was preserved, verifica- tion often failed or contained redundancies

  116. [126]

    NL to Temporal Logic Translation Developed an automatic translation mechanism from natural language sentences to temporal logic for formal verification. Table 2. Summary of LLMs related literature: Tools, Frameworks, and Achievements Working Document - Formalising Software Req...

  117. [127]

    ANTONIO toolkit A comprehensive analysis of NLP verification approaches and intro- duces a structured NLP Verification Pipeline with six key compo- nents. The work includes identifying gaps in existing methods, propos- ing novel solutions for improved robustness, extending sta...

  118. [128]

    Lemur Integrated LLMs with automated reasoners for program verification, defining sound transition rules and demonstrating improved perfor- mance on benchmark tests

  119. [129]

    Systematic Review Conducted a comprehensive review on natural language to formal specification translation, analyzing research across multiple academic databases

  120. [130]

    LLM-based Safety Require- ments Pipeline Designed a pipeline using LLMs to refine and decompose safety require- ments for autonomous vehicles, evaluated through expert assessments and industrial implementation

  121. [131]

    Specification Consistency Framework Ensured consistency between oral and formal specifications, incorporat- ing time extraction, input-output partitioning, and semantic reasoning, with positive evaluation results

  122. [132]

    Found that Stanford CoreNLP, FreeLing, and NLTK performed best

    NLP Tools for TFM Evaluated six NLP pipelines for Topological Functioning Modelling (TFM). Found that Stanford CoreNLP, FreeLing, and NLTK performed best

  123. [133]

    GPT-4 achieved best results with retrieval- augmented CoT prompt, producing 153 verified Dafny solutions

    LLM-based Dafny Task Generation Used LLMs (GPT-4, PaLM-2) to generate Dafny tasks from MBPP benchmark using different prompting strategies (context-less, signature, retrieval-augmented CoT). GPT-4 achieved best results with retrieval- augmented CoT prompt, producing 153 verifi...

  124. [134]

    Developed ReProver, a retrieval-augmented LLM- based prover that improved theorem proving efficiency

    LeanDojo & ReProver Introduced LeanDojo, an open-source toolkit for interacting with the Lean theorem prover. Developed ReProver, a retrieval-augmented LLM- based prover that improved theorem proving efficiency. Created a bench- mark with 98,734 theorems and proofs for testing...

  125. [135]

    Hammers are implemented to find the appropri- ate premises to complete the proofs of conjectures

    Thor and class methods named Hammers Introduced a framework named Thor which integrates language models with theorem provers. Hammers are implemented to find the appropri- ate premises to complete the proofs of conjectures. Datasets used are PISA and MiniF2F

  126. [136]

    Not specified The work proposes the integration of major formal languages (Dafny, Ada/SPARK, Frama-C, and KeY), their interactive theorem provers (Coq, Isabelle/HOL, Lean) with Copilot

  127. [137]

    This is based on literature available of ten years (2008 - 2018)

    Systematic Review Conducted a comprehensive survey on formal specification and verifica- tion of autonomous robotic systems in 2018. This is based on literature available of ten years (2008 - 2018)

    2018

  128. [138]

    PathCrawler gener- ated more context-aware annotations while, EVA efficiency improved having less run-time errors

    Symbolic analysis and LLMs prompts The quality of annotations produced in ACSL format is measured for PathCrawler and EVA (tools available in Frama-C). PathCrawler gener- ated more context-aware annotations while, EVA efficiency improved having less run-time errors. Table 3. S...

  129. [139]

    Dynamic Requirements Traceability Model Proposed a model to improve software quality through verification and validation of functional requirements, addressing scalability for both small and large projects

  130. [140]

    Early Phase Traceability and Verification Model Introduced a model for early development phase traceability and verifi- cation, with enhanced adaptability to requirement changes and impact analysis

  131. [141]

    Comprehensive Review Reviewed software requirements traceability, covering elements, chal- lenges, techniques, classified approaches, and identified future research directions

  132. [142]

    Empirical Analysis with Traceability Metrics Conducted an empirical study enforcing requirements completeness, introducing traceability metrics and regression analysis to quantify software quality and reduce defect rates

  133. [143]

    RETRO Developed RETRO, a tool for automating RTM generation, significantly improving accuracy and efficiency over manual tracing methods

  134. [144]

    VSM + BTM-GA Hybrid Ap- proach Proposed a hybrid method for traceability link generation that outper- formed traditional IR techniques, particularly in agile development, enhancing recall and precision

  135. [145]

    Trustrace Introduced a trust-based traceability recovery approach using mined repository data, achieving better precision and recall than standard IR methods

  136. [146]

    Deep Learning-Based Traceability (BI-GRU) Applied deep learning with BI-GRU for traceability, incorporating se- mantic understanding and domain knowledge, outperforming VSM and LSI methods

  137. [147]

    Topology-Based Model- Driven Approach Presented a topology-based, model-driven traceability technique for- malising specifications and establishing trace links between real-world functions and software artifacts

  138. [148]

    Event-Based Traceability Mechanism Proposed a mechanism to support software evolution through event- based artifact linking, improving change management performance and maintaining consistency in distributed environments

  139. [149]

    Tracebok Introduced a traceability body of knowledge framework categorising traceability approaches and offering practical guidance for software projects

  140. [150]

    Traceability Visualisation Review Reviewed visualisation tools and techniques, identifying issues such as scalability and visual clutter, and suggesting ways to improve traceabil- ity visualisation. Table 4. Summary of Other Sections of Literature Review: Tools, Frameworks, an...

  141. [151]

    Let’s think step by step

    Zero-Shot CoT Demonstrated that zero-shot prompts with simple additions like “Let’s think step by step” can significantly enhance LLM reasoning without training examples

  142. [152]

    One-Shot Prompting Used a single example to guide LLMs in generating desired outputs, showing potential as an alternative to zero- and few-shot approaches

  143. [153]

    Few-Shot Evaluation Found that zero-shot prompting can outperform few-shot setups, chal- lenging assumptions on example-based prompting

  144. [154]

    Self-Consistent Few-Shot Prompting Showed that prompting with few examples isn’t always better and proposed techniques to refine few-shot reliability

  145. [155]

    Prompt Engineering Re- view Surveyed prompt engineering strategies, including multimodal prompts, adversarial prompting, and robustness evaluations

  146. [156]

    Chain of Thought (CoT) Proposed stepwise reasoning in prompts to improve LLM performance in tasks requiring logic, math, and symbolic manipulation

  147. [157]

    Lost-in-the-Middle Highlighted LLMs’ U-shaped attention patterns, warning against long prompts where important middle-context information may be over- looked

  148. [158]

    Retrieval Augmented Gen- eration (RAG) Introduced a method to retrieve relevant knowledge for augmenting prompts, enhancing performance on knowledge-intensive tasks

  149. [159]

    LoRA Proposed Low-Rank Adaptation for fine-tuning LLMs efficiently with- out retraining the entire model, supporting modular adaptability

  150. [160]

    Iterative Prompting Frame- work Proposed a context-aware iterative prompting method for LLMs in multi-step reasoning tasks, dynamically synthesizing prompts to im- prove reasoning accuracy

  151. [161]

    UTP Tutorial Provided an introduction to Unifying Theories of Programming (UTP) and the use of alphabetised relational calculus to describe imperative constructs such as Hoare logic and refinement calculus

  152. [162]

    Institutions Introduced institutions as a formal framework for modeling logical sys- tems, including results on signature gluing and constraints for abstract data types, contributing to the theory of specification languages

  153. [163]

    Circus Described Circus, a language combining CSP, Z, and imperative pro- gramming, formalised using UTP to refine concurrent systems

  154. [164]

    Runtime Verification for UAS Applied runtime verification in UAS traffic management, using formal requirements to validate system safety across subsystems, confirmed via flight simulations

  155. [165]

    UTP-Based RTEMS Verifica- tion Verified RTEMS real-time OS using Promela and SPIN, linking UTP semantics for test generation and discussing future directions in space- grade verification. Table 5. Summary of Other Sections of Literature Review: Tools, Frameworks, and Methodolo...

  156. [166]

    Isabelle/UTP Introduced Isabelle/UTP to mechanise UTP semantics, providing formal proof tools for various paradigms, supporting development of auto- mated verification tools

  157. [167]

    UML Testing Profile (UTP) Discussed use of UML and UTP for model-based testing of embedded systems, presenting algorithms for test artefact generation under re- source constraints

  158. [168]

    Java Model of RTEMS Presented a verified Java model for RTEMS’s priority inheritance pro- tocol using Java Pathfinder, fixing known issues like data races and deadlocks. Table 6. Summary of Other Sections of Literature Review: Tools, Frameworks, and Methodologies

  159. [2023]

    Large Language Models Based Automatic Synthesis of Software Specifications. (2023). arXiv:cs.SE/2304.09181 https://arxiv.org/abs/2304.09181

    2023 arXiv

  160. [2025]

    NLP Verification: Towards a General Methodology for Certifying Robustness. (2025). arXiv:cs.CL/2403.10144 https://arxiv.org/abs/2403.10144

    2025 arXiv

Pith tools

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