A Short Survey on Formalising Software Requirements using Large Language Models

Arshad Beg; Diarmuid O'Donoghue; Rosemary Monahan

REVIEW 3 major objections 4 minor 190 references

A Short Survey on Formalising Software Requirements using Large Language Models

T0 review · 3 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 surveys 35 studies of using large language models to formalise software requirements, and argues that assertion-level generation currently exceeds the reliability of full contract synthesis.

desk verdict A useful short survey with a serious table problem: the appendix classification tables misattribute many reference numbers, so the survey's map cannot be trusted until corrected. read the letter →

arxiv 2506.11874 v1 pith:JNPQTAYU submitted 2025-06-13 cs.SE

Arshad Beg , Diarmuid O'Donoghue , Rosemary Monahan This is my paper

classification cs.SE

keywords formalspecificationlargelanguagemodelssoftwarerequirementsassertiongenerationverificationliteraturesurveypromptengineeringneuro-symbolicmethods

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper is a focused survey of 35 key papers on using large language models (LLMs) to write formal specifications from natural-language software requirements. It organises the field by methodology—prompt-only, fine-tuned, verifier-in-loop, neuro-symbolic, baseline, and meta-analysis—and identifies emerging trends. A central observation is that LLMs are currently more reliable at generating small, well-scoped specifications such as helper assertions than at synthesising complete contracts or temporal-logic formulas. The paper concludes that the most promising future directions combine LLMs with external verifiers and theorem provers, along with improved prompting and iterative refinement.

What carries the argument

The central object is the structured literature review itself, organised by a methodological classification scheme (prompt-only, fine-tuned, verifier-in-loop, neuro-symbolic, baseline/manual, meta-analysis, and IDE integration). The argument is carried by the contrast between two synthesis categories: assertion-level generation, where the LLM supplies a local fact needed by a verifier, and full contract or temporal-logic synthesis, where the LLM must produce a complete specification. The survey uses this contrast, supported by summary tables in the appendix, to derive its main trend and future research agenda.

What would settle it

Inspect the appendix tables against the cited papers' own abstracts: a check of Table 5 alone finds entries such as reference [37] labeled 'Reasoning Topologies' when the text and reference list identify [37] as Laurel, the Dafny assertion generator; if a systematic check reveals many such mismatches, the survey's synthesis is not reliable.

Watch

Extended reading notes

Core claim

The paper's central claim is that the research area of LLM-assisted software specification has matured enough to be surveyed and categorised, and that within it a clear reliability gradient exists. When the surveyed evidence is grouped, tasks like generating helper assertions (Laurel, AssertLLM) show high success rates—over 50% and 89% respectively—while full contract generation, such as producing VeriFast-compatible C specifications or translating natural language to LTL, often yields outputs that are only partially correct or fail verification. The paper interprets this as a consequence of task scope: smaller assertion-generation tasks give the LLM limited context and reduced complexity, whereas full contracts require broader abstraction and contextual understanding. It concludes that the field's trajectory points toward hybrid neuro-symbolic systems, fine-tuned prompts, and verifier-aware integration to close the gap between natural-language requirements and rigorous formal specifications.

Load-bearing premise

The survey's conclusions depend on the appendix tables and in-text citations correctly assigning each described tool and result to the actual paper being referenced.

Editorial extensions

If this is right

Teams using LLMs for specification can expect the most immediate payoff from tools that generate missing assertions or lemmas inside verifiers, as Laurel does for Dafny, rather than from asking the model for complete contracts.
Full contract synthesis will typically require iterative refinement, mutation operators, or human-in-the-loop correction, as exemplified by SpecGen and nl2spec, before the results are verifiable.
Combining LLMs with external SMT solvers or theorem provers—the neuro-symbolic approach—is a more reliable route to correct specifications than prompting alone.
The next generation of tools should integrate LLMs more tightly with verification feedback loops, since the survey finds that verifier-in-loop systems already outperform prompt-only systems on several benchmarks.

Reading between the lines

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

One testable extension is to benchmark assertion-generation and contract-synthesis tools on the same requirement suite under identical prompting conditions, to confirm that the reliability gap is due to task scope rather than to differences in how each tool was engineered.
The survey's classification suggests a practical deployment roadmap: start with LLM-suggested assertions for existing provers, then graduate to contract generation only after the verifier-in-loop feedback has been established.
A natural follow-up would be a live benchmark repository that pairs each methodological category with standard datasets and metrics, allowing new methods to be compared against the results summarised here.

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.

Desk Editor's Note

read the letter

Quick take: ignore the tables until they are fixed. The prose summaries in Section 4 are mostly faithful to the cited papers, and the Dafny running example is easy to follow. But Appendix Tables 2-5, which are the survey's actual deliverable, have pervasive reference-number misassignments. Table 5 alone labels [37] as "Reasoning Topologies" when [37] is Laurel; [48] as nl2spec when [48] is Quan's Explanation-Refiner; [6] as a prompt engineering survey when [6] is the DO-178C standard; [2] as GPT-3.5 code verification when [2] is Arora et al. The same kind of shuffling appears in Table 2, where [27] gets the SWOT analysis description and [3] gets the symbolic vs. ChatGPT description. A reader who trusts the tables will attribute results to the wrong papers. This is not cosmetic: the paper's stated value is to give readers an organized map of the literature, and the map is currently misleading.

What does work: the short narrative summaries in Section 4 mostly line up with the right citations. The Laurel example in Section 2 is a helpful concrete anchor. The discussion of assertion generation being more reliable than full contract synthesis is a reasonable reading of the surveyed results, though it is a narrative generalization from a non-systematic sample.

The soft spots beyond the tables: the methodology is described as a structured review, but the search and selection process is thin -- five databases, one AI tool, and a manual pass. That is acceptable for a short survey but overstates the rigor. There is no explicit validity check on the classification, and some newly added prompt-engineering references in the future-directions section are not part of the 35-paper corpus, so the survey's scope is fuzzy.

Who this is for: people wanting a quick orientation into LLMs for formal specification, provided they treat the tables as unreliable until corrected. It is not a research contribution and does not change practice.

My recommendation: send it to peer review with a clear request to fix the reference tables. The topic is useful, the narrative is readable, and the table problem is mechanical and fixable. A serious referee would catch this quickly. As it stands, I would not cite the survey's tables.

Referee Report

3 major / 4 minor

Summary. This paper is a short literature survey on the use of large language models (LLMs) to assist in formalising software requirements. It defines two research questions (RQ1: what methodologies transform natural language requirements into formal notations; RQ2: what are emerging trends and future directions), presents a motivating Dafny example, describes a literature-search methodology that uses academic databases and the Elicit tool, and then organises the surveyed literature into methodological categories. The paper concludes with observations about the current reliability of assertion generation versus full contract synthesis, and with a set of future research directions centred on prompt engineering, chain-of-thought reasoning, and hybrid neuro-symbolic systems.

Significance. If the survey's classifications were accurate, the paper would be a useful entry point for researchers and practitioners wishing to understand the current landscape of LLM-based formal specification. The paper has several strengths: it states clear research questions, includes a concrete Dafny working example, surveys a broad set of 61 references, and its narrative summaries in Section 4 mostly match the cited sources. However, the survey's central deliverable—the classification tables in Appendix 8.2—is not reliable because reference numbers are systematically misassigned, and this undermines the paper's claim to provide an accurate and organised summary of the literature.

major comments (3)

[Appendix 8.2, Table 5] continued from above: The survey's value proposition is precisely to give readers an accurate map of the literature, so this issue is load-bearing and must be fixed before the survey can be used.
[Table 2 and Table 4] The narrative text in Section 4.4 correctly attributes the symbolic-NLP-versus-ChatGPT comparison to [27], which makes the discrepancy with Table 2 particularly evident.
[Table 1 and Table 5] The abstract claims the survey presents 'a summary of thirty-five key papers', but Table 5 alone contains over sixty entries; the selection criterion for the 'key' subset should be clarified or the count should be aligned with the actual tables.

minor comments (4)

[Section 3] The methodology reports per-database result counts (17, 20, 595, 1,368, and 14,800) but does not state the exact search strings, the search date, or the inclusion/exclusion criteria in a reproducible form; please provide these details so that the search can be replicated.
[Section 5.1] The sentence 'some studies e.g. [60] show that zero-shot can outperform the few-shot case[61]' is misleading: reference [60] (Ye and Durrett) is about the unreliability of explanations in few-shot prompting, not a direct zero-shot-versus-few-shot performance comparison; please rephrase or cite a study that actually supports that claim.
[Abstract and Appendix 8.2] Please reconcile the abstract's statement of 'thirty-five key papers' with the appendix tables, which list more than sixty references; either restrict the tables to the key subset or state that the tables cover the full set of references found.
[Section 4 and Appendix tables] Several narrative statements in Section 4 are consistent with the bibliography (e.g., the description of Laurel in Section 4.6 matches [37]), so the tables should be carefully aligned with the narrative text; currently a reader cannot tell whether the text or the table is authoritative when they disagree.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular reasoning found; the survey's claims are summaries of independent external literature, with no fitted inputs, self-citation chains, or definitions that reduce to their own outputs.

full rationale

This paper is a literature survey. Its central deliverable is a classification and summary of thirty-five external papers, and its conclusions (e.g., that assertion generation is currently more reliable than full contract synthesis) are narrative generalizations from the surveyed papers rather than derivations from data the paper itself fits. No equations are derived, no parameters are fitted, and no prediction is made that reduces by construction to an input. The paper uses Elicit only as a screening tool, and every selected paper is manually reviewed; this does not create a circular dependency. While the reader's take and the skeptic headline identify real accuracy concerns about the appendix tables (e.g., Table 5 mislabels reference [37] as 'Reasoning Topologies' when it is Mugnier et al.'s Laurel paper), those are attribution/correctness problems, not circular reasoning: they do not make any claim equivalent to its own input by definition or by a self-citation chain. The paper also contains no load-bearing self-citations; references to VERIFAI are contextual, not evidential. Accordingly, the appropriate circularity score is 0.

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

A review paper introduces no free parameters or invented entities; its claims rest on the accuracy of the selection and summarization process.

assumptions (2)

domain assumption The manual screening and Elicit recommendations produced a representative and accurate set of 35 papers.
The survey's value depends on this selection being correct and representative, but the selection criteria are not fully specified in Section 3.
domain assumption The summaries in the paper accurately reflect the content of the cited papers.
Given the misattributions in the appendix tables, this assumption is not fully met, and the reader cannot always trust the summaries as a faithful guide.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A Short Survey on Formalising Software Requirements using Large Language Models." pith.science (2026). https://pith.science/paper/JNPQTAYU

@misc{pith2026250611874,
  author       = {Pith},
  title        = {Pith review of: A Short Survey on Formalising Software Requirements using Large Language Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JNPQTAYU}},
  note         = {Machine review of arXiv:2506.11874}
}

read the original abstract

This paper presents a focused literature survey on the use of large language models (LLM) to assist in writing formal specifications for software. A summary of thirty-five key papers is presented, including examples for specifying programs written in Dafny, C and Java. This paper arose from the project VERIFAI - Traceability and verification of natural language requirements that addresses the challenges in writing formal specifications from requirements that are expressed in natural language. Our methodology employed multiple academic databases to identify relevant research. The AI-assisted tool Elicit facilitated the initial paper selection, which were manually screened for final selection. The survey provides valuable insights and future directions for utilising LLMs while formalising software requirements.

Figures

Figures reproduced from arXiv: 2506.11874 by the authors.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

190 extracted references · 42 canonical work pages

[37]

Mugnier, E., Gonzalez, E.A., Jhala, R., Polikarpova, N., Zhou, Y.: Laurel: Generating dafny assertions using large language models (2024),https://arxiv.org/abs/2405.16792

arXiv 2024
[48]

Quan, X., Valentino, M., Dennis, L.A., Freitas, A.: Verification and refinement of natural language explanations through llm-symbolic theorem proving (2024),https://arxiv.org/abs/2405.01379

arXiv 2024
[6]

Ada Lett.31(3), 5–6 (Nov 2011)

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

work page arXiv 2011
[2]

Arora, C., Grundy, J., Abdelrazek, M.: Advancing requirements engineering through generative ai: Assessing the role of llms (2023),https://arxiv.org/abs/2310.13976

arXiv 2023
[27]

In: 2023 53rd Annual IEEE/IFIP International Conference on Dependable Sys- temsandNetworksWorkshops(DSN-W).pp.259–262(2023)

Leong, I.T., Barbosa, R.: Translating natural language requirements to formal specifications: A study on gpt and symbolic nlp. In: 2023 53rd Annual IEEE/IFIP International Conference on Dependable Sys- temsandNetworksWorkshops(DSN-W).pp.259–262(2023). https://doi.org/10.1109/DSN-W58399. 2023.00065

arXiv 2023
[3]

In: Proceedings of the ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems

Arora, C., Sabetzadeh, M., Briand, L., Zimmer, F.: 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. p. 250–260. MODELS ’16, Associ- ation for Computing Machinery, New York, NY, USA (2016).https://...

arXiv 2016
[1]

Amatriain, X.: Prompt design and engineering: Introduction and advanced methods (2024),https: //arxiv.org/abs/2401.14423

arXiv 2024
[4]

In: Proceedings of the 10th Australian Workshop on Safety Critical Systems and Software - Volume 55

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

2006

Show all 190 references

[5]

CoRRabs/2401.14295 (2024)

Besta, M., Memedi, F., Zhang, Z., Gerstenberger, R., Blach, N., Nyczyk, P., Copik, M., Kwasniewski, G., Müller, J., Gianinazzi, L., Kubicek, A., Niewiadomski, H., Mutlu, O., Hoefler, T.: Topologies of reasoning: Demystifying chains, trees, and graphs of thoughts. CoRRabs/2401....

2024 doi
[7]

In: Service-Oriented Computing: 22nd Inter- nationalConference,ICSOC2024,Tunis,Tunisia,December3–6,2024,Proceedings,PartII.p.357–372

Caglayan, B., Wang, M., Kelleher, J.D., Fei, S., Tong, G., Ding, J., Zhang, P.: Bis: Nl2sql service evaluation benchmark for business intelligence scenarios. In: Service-Oriented Computing: 22nd Inter- nationalConference,ICSOC2024,Tunis,Tunisia,December3–6,2024,Proceedings,Par...

2024 doi
[8]

Casadio, M., Dinkar, T., Komendantskaya, E., Arnaboldi, L., Daggitt, M.L., Isac, O., Katz, G., Rieser, V., Lemon, O.: Nlp verification: Towards a general methodology for certifying robustness (2025),https: //arxiv.org/abs/2403.10144

2025 arXiv
[9]

Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., Trippel, C.: nl2spec: Interactively translating unstruc- tured natural language to temporal logics with large language models (2023),https://arxiv.org/abs/ 2303.04864

2023 arXiv
[10]

In: SoutheastCon 2024

Couder, J.O., Gomez, D., Ochoa, O.: Requirements verification through the analysis of source code by large language models. In: SoutheastCon 2024. pp. 75–80 (March 2024).https://doi.org/10.1109/ SoutheastCon52093.2024.10500073

2024
[11]

Elicit: Elicit - the ai research assistant.https://www.elicit.com, accessed: 2025-04-11 at 1249PM

2025
[12]

In: Lerner, B.S., Bodík, R., Krishnamurthi, S

Ernst, M.D.: Natural Language is a Programming Language: Applying Natural Language Process- ing to Software Development. In: Lerner, B.S., Bodík, R., Krishnamurthi, S. (eds.) 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Inf...

2017 doi
[13]

Fan, W., Rego, M., Hu, X., Dod, S., Ni, Z., Xie, D., DiVincenzo, J., Tan, L.: Evaluating the ability of large language models to generate verifiable specifications in verifast (2025),https://arxiv.org/abs/ 2411.02318

2025 arXiv
[14]

Fang,W.,Li,M.,Li,M.,Yan,Z.,Liu,S.,Zhang,H.,Xie,Z.:Assertllm:Generatinghardwareverification assertionsfromdesignspecificationsviamulti-llms.In:2024IEEELLMAidedDesignWorkshop(LAD). pp. 1–1 (2024).https://doi.org/10.1109/LAD62341.2024.10691792

2024
[15]

In: Proceedings of the 39th IEEE/ACM In- ternational Conference on Automated Software Engineering

Fazelnia, M., Mirakhorli, M., Bagheri, H.: Translation titans, reasoning challenges: Satisfiability-aided language models for detecting conflicting requirements. In: Proceedings of the 39th IEEE/ACM In- ternational Conference on Automated Software Engineering. p. 2294–2298. AS...

2024
[16]

32(2), 113–133 (Feb 2002).https://doi.org/10.1002/spe.430, https://doi.org/10.1002/spe.430

Gervasi,V.,Nuseibeh,B.:Lightweightvalidationofnaturallanguagerequirements.Softw.Pract.Exper. 32(2), 113–133 (Feb 2002).https://doi.org/10.1002/spe.430, https://doi.org/10.1002/spe.430

2002 doi
[17]

In: Rayadurgam, S., Tkachuk, O

Ghosh, S., Elenius, D., Li, W., Lincoln, P., Shankar, N., Steiner, W.: Arsenal: Automatic requirements specification extraction from natural language. In: Rayadurgam, S., Tkachuk, O. (eds.) NASA Formal Methods. pp. 41–46. Springer International Publishing, Cham (2016)

2016
[18]

In: Kosmatov, N., Kovács, L

Granberry, G., Ahrendt, W., Johansson, M.: Specify what? enhancing neural specification synthesis by symbolic methods. In: Kosmatov, N., Kovács, L. (eds.) Integrated Formal Methods. pp. 307–325. Springer Nature Switzerland, Cham (2025)

2025
[19]

In: Margaria, T., Steffen, B

Granberry, G., Ahrendt, W., Johansson, M.: Towards integrating copiloting and formal methods. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification. pp. 144–158. Springer Nature Switzerland, ...

2025
[20]

In- formation Systems 11(1), 9–23 (1986)

Greenspan, S.J., Borgida, A., Mylopoulos, J.: A requirements modeling language and its logic. In- formation Systems 11(1), 9–23 (1986). https://doi.org/https://doi.org/10.1016/0306-4379(86) 90020-7, https://www.sciencedirect.com/science/article/pii/0306437986900207

1986
[21]

Hahn, C., Schmitt, F., Tillman, J.J., Metzger, N., Siber, J., Finkbeiner, B.: Formal specifications from natural language (2022),https://arxiv.org/abs/2206.01962

2022 arXiv
[22]

In: Ku, L., Martins, A., Srikumar, V

Hsieh, C., Chuang, Y., Li, C., Wang, Z., Le, L.T., Kumar, A., Glass, J.R., Ratner, A., Lee, C., Krishna, R., Pfister, T.: Found in the middle: Calibrating positional attention bias improves long context utiliza- tion. In: Ku, L., Martins, A., Srikumar, V. (eds.) Findings of th...

2024 doi
[23]

Hu, E.J., Shen, Y., Wallis, P., Allen-Zhu, Z., Li, Y., Wang, S., Wang, L., Chen, W.: Lora: Low-rank adaptation of large language models. In: The Tenth International Conference on Learning Represen- A Short Survey on Formalising Software Requirements with Large Language Models ...

2022
[24]

a travel guide (2024), https://arxiv.org/abs/2002.07279

Huisman, M., Gurov, D., Malkis, A.: Formal methods: From academia to industrial practice. a travel guide (2024), https://arxiv.org/abs/2002.07279

2024 arXiv
[25]

In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A

Jiang, A.Q., Li, W., Tworkowski, S., Czechowski, K., Odrzygóźdź, T., Mił oś, P., Wu, Y., Jamnik, M.: Thor: Wielding hammers to integrate language models and automated theorem provers. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Ne...

2022
[26]

In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A

Kojima, T., Gu, S.S., Reid, M., Matsuo, Y., Iwasawa, Y.: Large language models are zero-shot reasoners. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information Processing Systems. vol. 35, pp. 22199–22213. Curran Associates...

2022
[28]

IEEE Transactions on Software Engineering 40(8), 818–840 (2014)

Leopold, H., Mendling, J., Polyvyanyy, A.: Supporting process model validation through natural language generation. IEEE Transactions on Software Engineering 40(8), 818–840 (2014). https: //doi.org/10.1109/TSE.2014.2327044

2014
[29]

In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H

Lewis, P., Perez, E., Piktus, A., Petroni, F., Karpukhin, V., Goyal, N., Küttler, H., Lewis, M., Yih, W., Rocktäschel, T., Riedel, S., Kiela, D.: Retrieval-augmented generation for knowledge-intensive NLP tasks. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H....

2020
[30]

ACM Trans

Li, J., Li, G., Li, Y., Jin, Z.: Structured chain-of-thought prompting for code generation. ACM Trans. Softw. Eng. Methodol.34(2) (Jan 2025). https://doi.org/10.1145/3690635, https://doi.org/10. 1145/3690635

2025 doi
[31]

Li, M., Fang, W., Zhang, Q., Xie, Z.: Specllm: Exploring generation and review of vlsi design specifi- cation with large language model (2024),https://arxiv.org/abs/2401.13266

2024 arXiv
[32]

Li, Y., Hui, B., Xia, X., Yang, J., Yang, M., Zhang, L., Si, S., Chen, L.H., Liu, J., Liu, T., Huang, F., Li, Y.: One-shot learning as instruction data prospector for large language models (2024),https: //arxiv.org/abs/2312.10302

2024 arXiv
[33]

ACM Comput

Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: A survey. ACM Comput. Surv.52(5) (Sep 2019).https://doi.org/10. 1145/3342355, https://doi.org/10.1145/3342355

2019 doi
[34]

Ma, L., Liu, S., Li, Y., Xie, X., Bu, L.: Specgen: Automated generation of formal program specifications via large language models (2024),https://arxiv.org/abs/2401.08807

2024 arXiv
[35]

org/abs/2304.09181

Mandal,S.,Chethan,A.,Janfaza,V.,Mahmud,S.M.F.,Anderson,T.A.,Turek,J.,Tithi,J.J.,Muzahid, A.: Large language models based automatic synthesis of software specifications (2023),https://arxiv. org/abs/2304.09181

2023 arXiv
[36]

Misu, M.R.H., Lopes, C.V., Ma, I., Noble, J.: Towards ai-assisted synthesis of verified dafny methods. Proc. ACM Softw. Eng.1(FSE) (Jul 2024). https://doi.org/10.1145/3643763, https://doi.org/ 10.1145/3643763

2024 doi
[38]

Mukherjee, P., Delaware, B.: Towards automated verification of llm-synthesized c programs (2024), https://arxiv.org/abs/2410.14835

2024
[39]

Nayak, A., Timmapathini, H.P., Murali, V., Ponnalagu, K., Venkoparao, V.G., Post, A.: Req2spec: Transforming software requirements into formal specifications using natural language processing. In: Requirements Engineering: Foundation for Software Quality: 28th International Wo...

2022
[40]

In: Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering

Nazaruka, E., Osis, J.: 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. p. 501–512. ENASE 2018, SCITEPRESS - Scie...

2018 doi
[41]

https://doi.org/10.3390/ electronics13112055, https://www.mdpi.com/2079-9292/13/11/2055

Necula, S.C., Dumitriu, F., Greavu-S,erban, V.: A systematic literature review on using natural language processinginsoftwarerequirementsengineering.Electronics 13(11)(2024). https://doi.org/10.3390/ electronics13112055, https://www.mdpi.com/2079-9292/13/11/2055

2024
[42]

In: Alur, R., Henzinger, T.A

Nelken, R., Francez, N.: Automatic translation of natural language system specifications into temporal logic. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification. pp. 360–371. Springer Berlin Heidelberg, Berlin, Heidelberg (1996)

1996
[43]

In: 2024 IEEE 32nd International Requirements Engineering Conference (RE)

Nouri, A., Cabrero-Daniel, B., Törner, F., Sivencrona, H., Berger, C.: Engineering safety requirements for autonomous driving with large language models. In: 2024 IEEE 32nd International Requirements Engineering Conference (RE). pp. 218–228 (2024).https://doi.org/10.1109/RE590...

2024
[44]

Computer Science and Information Systems10(4), 1499–1524 (2013)

Nowakowski, W., Śmiałek, M., Ambroziewicz, A., Straszak, T.: Requirements-level language and tools for capturing software system essence. Computer Science and Information Systems10(4), 1499–1524 (2013)

2013
[45]

In: Pro- ceedings of the Second International Conference on Requirements Engineering

Osborne, M., MacNish, C.: Processing natural language software requirement specifications. In: Pro- ceedings of the Second International Conference on Requirements Engineering. pp. 229–236 (1996). https://doi.org/10.1109/ICRE.1996.491451

1996
[46]

In: 6th IET International Conference on System Safety 2011

Palin, R., Ward, D., Habli, I., Rivett, R.: Iso 26262 safety cases: Compliance and assurance. In: 6th IET International Conference on System Safety 2011. pp. 1–6 (2011).https://doi.org/10.1049/cp. 2011.0251

2011
[47]

In: Proceedings of the 21st International Conference on Mining Software Repositories

Preda, A.R., Mayr-Dorn, C., Mashkoor, A., Egyed, A.: Supporting high-level to low-level requirements coverage reviewing with large language models. In: Proceedings of the 21st International Conference on Mining Software Repositories. p. 242–253. MSR ’24, Association for Comput...

2024
[49]

Reinpold, L.M., Schieseck, M., Wagner, L.P., Gehlhoff, F., Fay, A.: Exploring llms for verifying technical system specifications against requirements (2024),https://arxiv.org/abs/2411.11582

2024 arXiv
[50]

In: Bouamor, H., Pino, J., Bali, K

Shum, K., Diao, S., Zhang, T.: Automatic prompt augmentation and selection with chain-of-thought from labeled data. In: Bouamor, H., Pino, J., Bali, K. (eds.) Findings of the Association for Compu- tational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023. pp. 12113–121...

2023 doi
[51]

Tihanyi, N., Jain, R., Charalambous, Y., Ferrag, M.A., Sun, Y., Cordeiro, L.C.: A new era in software security: Towards self-healing software via large language models and formal verification (2024),https: //arxiv.org/abs/2305.14752

2024 arXiv
[52]

In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A

Wei, J., Wang, X., Schuurmans, D., Bosma, M., ichter, b., Xia, F., Chi, E., Le, Q.V., Zhou, D.: Chain- of-thought prompting elicits reasoning in large language models. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information...

2022
[53]

CoRR abs/2302.11382 (2023)

White, J., Fu, Q., Hays, S., Sandborn, M., Olea, C., Gilbert, H., Elnashar, A., Spencer-Smith, J., Schmidt, D.C.: A prompt pattern catalog to enhance prompt engineering with chatgpt. CoRR abs/2302.11382 (2023). https://doi.org/10.48550/ARXIV.2302.11382, https://doi.org/ 10.485...

2023 doi arXiv
[54]

Wu, H., Barrett, C., Narodytska, N.: Lemur: Integrating large language models in automated program verification (2024), https://arxiv.org/abs/2310.04870

2024 arXiv
[55]

CoRR abs/2305.09993 (2023)

Xu, W., Banburski-Fahey, A., Jojic, N.: Reprompting: Automated chain-of-thought prompt inference through gibbs sampling. CoRR abs/2305.09993 (2023). https://doi.org/10.48550/ARXIV.2305. 09993, https://doi.org/10.48550/arXiv.2305.09993

2023 doi arXiv
[56]

In: 2024 IEEE 24th International Conference on Software Quality, Reliability and Security (QRS)

Xu, Y., Feng, J., Miao, W.: 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). pp. 204–215 (2024). https://...

2024
[57]

In: 2015 Design, Automation & Test in Europe Conference & Exhibition (DATE)

Yan, R., Cheng, C.H., Chai, Y.: Formal consistency checking over specifications in natural languages. In: 2015 Design, Automation & Test in Europe Conference & Exhibition (DATE). pp. 1677–1682 (2015)

2015
[58]

In: Oh, A., Naumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S

Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R.J., Anandkumar, A.: Leandojo: Theorem proving with retrieval-augmented language models. In: Oh, A., Naumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. (eds.) Advances in Neural Infor...

2023
[59]

In: 2024 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR)

Yao, J., Liu, Y., Dong, Z., Guo, M., Hu, H., Keutzer, K., Du, L., Zhou, D., Zhang, S.: Promptcot: Align prompt distribution via adapted chain-of-thought. In: 2024 IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR). pp. 7027–7037 (2024).https://doi.org/10.110...

2024
[60]

In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A

Ye, X., Durrett, G.: The unreliability of explanations in few-shot prompting for textual reasoning. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information Processing Systems. vol. 35, pp. 30378–30392. Curran Associates, In...

2022
[61]

"+s2).value.1 ==

Zhang, H., Cai, M., Zhang, X., Zhang, C.J., Mao, R., Wu, K.: Self-convinced prompting: Few-shot question answering with repeated introspection (2023),https://arxiv.org/abs/2310.05035 14 Arshad Beg, Diarmuid O’Donoghue, and Rosemary Monahan 8 Appendices 8.1 Dafny Lemma Definiti...

2023 arXiv
[62]

LLM-based Code VerificationUses LLMs like GPT-3.5 to verify code by analyzing requirements and explaining whether they are met
[63]

nl2spec A framework leveraging LLMs to generate formal specifications from natural lan- guage, addressing ambiguity in system requirements with iterative refinement
[64]

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
[65]

Not Specified Analyzesresearchdirectionsinsoftwarerequirementengineering,conductingaSWOT analysis and sharing evaluation findings
[66]

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

Symbolic NLP vs. ChatGPTCompares the performance of symbolic NLP and ChatGPT in generating correct JML output from natural language preconditions
[67]

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

SpecSyn A framework using LLMs for automatic synthesis of software specifications, improving accuracy by 21% over previous tools
[69]

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

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

SpecLLM Explores using LLMs for generating and reviewing VLSI design specifications, im- proving chip design documentation
[72]

Requirements Specification Lan- guage (RSL), ReDSeeDS Enhanced software requirements specification using constrained natural language and automated transformations into code
[73]

ARSENAL Framework and Methodology Automated extraction of requirements specification from natural language with au- tomatic verification
[74]

BPM-to-NL Translation ProcessGenerated natural language descriptions from business process models for better val- idation
[75]

Laurel A framework to generate Dafny assertions to automate program verification process for a SMT solver
[76]

Controlled Natural Language (CL) with ANLT Expressed software requirements in a limited set of natural language and translated to logical expressions to detect ambiguities
[77]

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%
[78]

NL-to-LTL Translation via LLMsConverted unstructured natural language requirements to NL-LTL pairs, achieving 94.4% accuracy on public datasets
[79]

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

LLM-based Formal Specifications Translation Translated natural language into formal rules (regex, FOL, LTL) with high adapt- ability and performance
[81]

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

LLM-based Requirement Cover- age Analysis Ensured low-level software requirements met high-level requirements, achieving 99.7% recall in spotting missing coverage
[83]

Table 2: Summary of LLMs related literature (Part 1 of 2) 16 Arshad Beg, Diarmuid O’Donoghue, and Rosemary Monahan Ref

SAT-LLM Integrated SMT solvers with LLMs to improve conflict identification in requirements; significantly outperformed standalone LLMs in detecting complex conflicts. Table 2: Summary of LLMs related literature (Part 1 of 2) 16 Arshad Beg, Diarmuid O’Donoghue, and Rosemary Mo...
[84]

NLP for Software DevelopmentAssessed NLP techniques for various software development stages, highlighting their suitability for generating assertions and processing developer queries
[85]

Req2Spec NLP-basedtoolthatformalisesnaturallanguagerequirementsforHANFOR;achieved 71% accuracy in formalising 222 automotive requirements at BOSCH
[86]

RML (Requirements Modeling Language) Introduced a conceptual model-based framework ensuring precision, consistency, and clarity in requirements writing
[87]

GPT-4o for VeriFast VerificationEvaluated GPT-4o’s ability to generate C program specifications for VeriFast; found that while functional behavior was preserved, verification often failed or contained redundancies
[88]

NL to Temporal Logic Transla- tion Developed an automatic translation mechanism from natural language sentences to temporal logic for formal verification
[89]

ANTONIO toolkit A comprehensive analysis of NLP verification approaches and introduces a structured NLP Verification Pipelinewith six key components. The work includes identi- fying gaps in existing methods, proposing novel solutions for improved robustness, extending standard...
[90]

Lemur Integrated LLMs with automated reasoners for program verification, defining sound transition rules and demonstrating improved performance on benchmark tests
[91]

Systematic Review Conducted a comprehensive review on natural language to formal specification trans- lation, analyzing research across multiple academic databases
[92]

LLM-based Safety Requirements Pipeline Designed a pipeline using LLMs to refine and decompose safety requirements for au- tonomous vehicles, evaluated through expert assessments and industrial implementa- tion
[93]

Specification Consistency Frame- work Ensured consistency between oral and formal specifications, incorporating time ex- traction, input-output partitioning, and semantic reasoning, with positive evaluation results
[94]

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
[95]

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

LLM-based Dafny Task Genera- tion Used LLMs (GPT-4, PaLM-2) to generate Dafny tasks from MBPP benchmark us- ing different prompting strategies (context-less, signature, retrieval-augmented CoT). GPT-4 achieved best results with retrieval-augmented CoT prompt, producing 153 ver...
[96]

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 benchmark with 98,734 theorems and proofs for testing ge...
[97]

Hammers are implemented to find the appropriate 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 appropriate premises to complete the proofs of conjectures. Datasets used are PISA and MiniF2F
[98]

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
[99]

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

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

2018
[100]

PathCrawler generated 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 generated more context-aware annotations while, EVA efficiency improved having less run-time errors. Table 3: Sum...
[101]

Domain Model ExtractorFine-tuned Generates domain models from NL requirements; evaluated in an industrial case study for performance and accuracy
[102]

ChatGPTPrompt-only Compares symbolic NLP and ChatGPT in generating correct JML from NL preconditions

Symbolic NLP vs. ChatGPTPrompt-only Compares symbolic NLP and ChatGPT in generating correct JML from NL preconditions
[103]

BPM-to-NL TranslationPrompt-only Translates business process models to NL to support better stake- holder validation
[104]

Lemur Verifier-in-loop Integrates LLMs with automated reasoners and defines sound transition rules for verification
[105]

GPT-4o for VeriFast Verifica- tion Verifier-in-loop Assesses GPT-4o’s performance in generating C specs for Veri- Fast; captures issues in functional correctness
[106]

ARSENAL Fine-tuned Extracts requirements from NL and performs automatic verifica- tion
[107]

Laurel for Dafny Prompt-only + Verifier-in-loopAutomates generation of Dafny assertions to support SMT-based verification
[108]

PathCrawler + EVAVerifier-in-loop + PromptPathCrawlergeneratescontext-awareACSLannotations;EVAre- duces runtime errors in Frama-C
[109]

NL to Temporal Logic Transla- tion Prompt-only Automatically translates NL into temporal logic for formal veri- fication
[110]

Req2Spec Prompt-only Converts NL requirements into formal specs (e.g., HANFOR); 71% accuracy on BOSCH data
[111]

AssertLLM Multi-LLMs / Prompt-onlyUses 3 customized LLMs to generate assertions from hardware design specs; 89% correctness achieved
[112]

SpecSyn Fine-tuned Synthesizes software specifications from NL, improving over prior tools by 21%
[113]

nl2spec Prompt-only + Iterative RefinementIterativelygeneratesformalspecsfromNLrequirements,reducing ambiguity
[114]

LLM-basedRequirementCover- age Prompt-only Maps low-level requirements to high-level ones with 99.7% recall in coverage detection
[115]

SpecLLM Prompt-only Uses LLMs to create and review VLSI design specs, enhancing chip documentation
[116]

NL-to-LTL via LLMsPrompt-only Converts unstructured NL to NL-LTL pairs with 94.4% accuracy
[117]

ANTONIO Toolkit Verifier-in-loop Introduces an NLP Verification Pipeline with metrics, gaps, and semantic subspace verification proposals
[118]

GPT-3.5 for Code VerificationPrompt-only Uses GPT-3.5 to verify code against requirements, providing feed- back on requirement satisfaction
[119]

GPT-4o + Claude for Smart Grid Verifier-in-loop Applies GPT-4o and Claude 3.5 for smart grid requirement veri- fication, reaching 79–94% F1-scores
[120]

Systematic Review Meta-analysis Surveys NL-to-specification literature across domains and aca- demic sources
[121]

SAT-LLM Neuro-symbolic (LLM + SMT)Combines LLMs with SMT to detect complex conflicts in require- ments
[122]

Thor Neuro-symbolic Integrates LLMs with theorem provers using class methods like Hammers for proof completion
[123]

Dafny Task Gen w/ CoTPrompt + Retrieval + CoTGPT-4 and PaLM-2 generate verified Dafny tasks via retrieval- augmented CoT prompting
[124]

LeanDojo + ReProverRetrieval-augmented Retrieval-augmented LLM-based prover improves Lean theorem proving on 98K+ samples
[125]

SynVer for C Verifier-in-loop Synthesizes and verifies C programs using VST with improved automation
[126]

Copilot + Formal MethodsIDE Integration ProposalSuggests integrating formal tools (e.g., Dafny, Coq, KeY) into IDEs like Copilot
[127]

Robotic Systems ReviewMeta-analysis Reviews 10 years of literature on formal verification in au- tonomous robotic systems
[128]

NLP for Software DevSurvey / Meta-analysis Evaluates NLP techniques in software development life cycle
[129]

RML (1986) Manual / Controlled NLIntroduces controlled NL framework for precise and consistent requirements writing

1986
[130]

ESBMC-AI Neuro-symbolic Uses LLMs + formal verification to detect vulnerabilities in soft- ware
[131]

Specification Consistency Framework Manual / Baseline Alignsoralandformalspecificationsusingsemanticreasoningand input-output analysis
[132]

PipelinePrompt-only Uses LLMs to decompose and refine autonomous vehicle safety requirements

LLM Safety Req. PipelinePrompt-only Uses LLMs to decompose and refine autonomous vehicle safety requirements
[133]

18 Arshad Beg, Diarmuid O’Donoghue, and Rosemary Monahan Table 5: Classification of Surveyed Literature by Methodology Ref

NLP Tools for TFM Prompt-only Compares NLP pipelines for topological modeling; CoreNLP and FreeLing perform best. 18 Arshad Beg, Diarmuid O’Donoghue, and Rosemary Monahan Table 5: Classification of Surveyed Literature by Methodology Ref. Tool / Work Classification
[134]

Prompt Engineering Survey Prompt-only
[135]

Advancing RE with LLMs Prompt-only
[136]

Domain Model Extractor Fine-tuned
[137]

IEC 61508 Safety Standard Not LLM-based
[138]

Reasoning Topologies Prompt-only
[139]

DO-178C Standard Not LLM-based
[140]

BIS NL2SQL Prompt-only
[141]

ANTONIO Toolkit Verifier-in-loop
[142]

nl2spec Prompt-only + Iterative Refinement
[143]

GPT-3.5 for Code Verification Prompt-only
[144]

Elicit Tool Tool Support (Meta)
[145]

NLP in Software Dev Survey / Meta-analysis
[146]

GPT-4o + VeriFast Verifier-in-loop
[147]

AssertLLM Multi-LLMs / Prompt-only
[148]

SAT-LLM Neuro-symbolic (LLM + SMT)
[149]

NASA SW Formal Verification Manual / Baseline
[150]

PathCrawler + EVA Verifier-in-loop + Prompt
[151]

Copilot + Formal Methods IDE Integration Proposal
[152]

RML (1986) Manual / Controlled NL

1986
[153]

NL to FOL, Regex, LTL Prompt-only
[154]

Long Context Calibration Prompt-only
[155]

LoRA Tuning Fine-tuned
[156]

Formal Methods Transfer Meta-analysis
[157]

Thor (LLM + Theorem Prover) Neuro-symbolic
[158]

Zero-shot Reasoning Prompt-only
[159]

Symbolic NLP vs ChatGPT Prompt-only
[160]

BPM to NL Translation Prompt-only
[161]

RAG for NLP Tasks Retrieval-augmented
[162]

Structured CoT for Code Prompt-only
[163]

One-shot Learning Prompt-only
[164]

Robotic Systems Review Meta-analysis
[165]

SpecGen Prompt + Mutation (Verifier-in-loop)
[166]

Dafny Task Gen w/ CoT Prompt + Retrieval + CoT
[167]

Laurel for Dafny Prompt-only + Verifier-in-loop
[168]

SynVer for C Verifier-in-loop
[169]

Req2Spec Prompt-only
[170]

NLP Tools for TFM Prompt-only
[171]

NL to Temporal Logic Fine-tuned
[172]

LLMs in Autonomous Driving Prompt-only
[173]

RSL + ReDSeeDS Fine-tuned / Controlled NL
[174]

Controlled NL (1996) Controlled NL

1996
[175]

ISO 26262 Not LLM-based
[176]

LLMs for Requirement Coverage Prompt-only
[177]

Explanation-Refiner Neuro-symbolic
[178]

GPT-4o / Claude 3.5 for Smart Grid Prompt-only
[179]

Automate-CoT Prompt-only + Automated CoT
[180]

ESBMC-AI Verifier-in-loop
[181]

Chain-of-Thought (CoT) Prompt-only
[182]

Prompt Pattern Catalog Prompt-only
[183]

Lemur (LLM + Verifier) Verifier-in-loop
[184]

Reprompting w/ Gibbs Prompt-only
[185]

NL to LTL (Dynamic Prompt) Prompt + Human-in-loop
[186]

NL Consistency Framework Fine-tuned
[187]

LeanDojo + ReProver Retrieval + Verifier-in-loop
[188]

PromptCoT Prompt-only
[189]

Explanation Failures in Few-Shot Prompt-only
[190]

Self-Convinced Prompting Prompt-only

Pith tools

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

[1] [37]

Mugnier, E., Gonzalez, E.A., Jhala, R., Polikarpova, N., Zhou, Y.: Laurel: Generating dafny assertions using large language models (2024),https://arxiv.org/abs/2405.16792

arXiv 2024

[2] [48]

Quan, X., Valentino, M., Dennis, L.A., Freitas, A.: Verification and refinement of natural language explanations through llm-symbolic theorem proving (2024),https://arxiv.org/abs/2405.01379

arXiv 2024

[3] [6]

Ada Lett.31(3), 5–6 (Nov 2011)

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

work page arXiv 2011

[4] [2]

Arora, C., Grundy, J., Abdelrazek, M.: Advancing requirements engineering through generative ai: Assessing the role of llms (2023),https://arxiv.org/abs/2310.13976

arXiv 2023

[5] [27]

In: 2023 53rd Annual IEEE/IFIP International Conference on Dependable Sys- temsandNetworksWorkshops(DSN-W).pp.259–262(2023)

Leong, I.T., Barbosa, R.: Translating natural language requirements to formal specifications: A study on gpt and symbolic nlp. In: 2023 53rd Annual IEEE/IFIP International Conference on Dependable Sys- temsandNetworksWorkshops(DSN-W).pp.259–262(2023). https://doi.org/10.1109/DSN-W58399. 2023.00065

arXiv 2023

[6] [3]

In: Proceedings of the ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems

Arora, C., Sabetzadeh, M., Briand, L., Zimmer, F.: 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. p. 250–260. MODELS ’16, Associ- ation for Computing Machinery, New York, NY, USA (2016).https://...

arXiv 2016

[7] [1]

Amatriain, X.: Prompt design and engineering: Introduction and advanced methods (2024),https: //arxiv.org/abs/2401.14423

arXiv 2024

[8] [4]

In: Proceedings of the 10th Australian Workshop on Safety Critical Systems and Software - Volume 55

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

2006