Pith. sign in

REVIEW 4 major objections 4 minor 1 cited by

Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision

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

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

Pith's one-line read ReDeFo argues that reliable automated code generation needs formal specifications as the connecting layer between requirements and code, produced by three specialized agents.

desk verdict A clearly-written vision paper for a three-agent formal-methods pipeline; no implementation, so judge it as a research agenda, not a validated system. read the letter →

arxiv 2508.18675 v1 pith:HEDVAEUV submitted 2025-08-26 cs.SE

Xu Lu , Weisong Sun , Yiran Zhang , Ming Hu , Cong Tian , Zhi Jin , Yang Liu This is my paper
classification cs.SE
keywords automatedcodegenerationformalspecificationlargelanguagemodelmulti-agentsystemsrequirementsengineeringverificationdevelopment
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 proposes ReDeFo, a multi-agent framework that aims to make automatically generated code reliable by inserting formal specification between natural language requirements and code. Rather than asking an LLM to jump directly from requirements to code, ReDeFo uses three agents with formal-methods knowledge: an Analyst that refines requirements, a Formalizer that translates them into precise specifications, and a Coder that generates and verifies code against those specifications. The authors argue that formal specifications make correctness provable rather than probabilistic, and they illustrate the workflow on a safety-critical aerospace mode-switching component, model-checking LTL properties with NuSMV and verifying ACSL-annotated C with Frama-C. The paper is a vision and architecture proposal, not an empirical evaluation; its contribution is the claim that a multi-agent, human-in-the-loop pipeline with formal specifications can close the correctness gap in LLM-based code generation.

What carries the argument

The load-bearing mechanism is the formal specification as the intermediate artifact. System-level behaviors are expressed as linear temporal logic (LTL) properties and checked with the NuSMV model checker; function-level behavior is expressed as ACSL (ANSI/ISO C Specification Language) contracts and verified deductively with Frama-C. This two-level formalization gives the Coder a precise semantic target and gives the pipeline a verification step that can detect hidden bugs and enforce critical properties. The human-in-the-loop checkpoints—reviewing refined requirements, verifying the architecture model, and adjusting low-level specifications from verification failures—are what keep the forma

What would settle it

Take a set of natural-language requirements with known reference implementations and apply the full ReDeFo pipeline. Count how often the generated code passes Frama-C and NuSMV verification yet fails to match human judgment of the original requirements on held-out behavioral tests. If even a single such divergence occurs, the central reliability claim—that verified code guarantees satisfaction of the natural-language intent—is falsified.

Watch

Extended reading notes

Core claim

The central claim is that formal specification should be the load-bearing intermediate artifact between natural language requirements and executable code, and that the transformation is best done by a collaborative pipeline of specialized agents rather than a single end-to-end LLM. The Analyst structures and slices requirements and produces architecture models; the Formalizer turns them into formal specifications; the Coder synthesizes modules and runs formal verification, yielding verified components and verification reports. The paper reports this as the first multi-agent framework for automated code generation with formal correctness guarantees, and supports plausibility with a worked cas

Load-bearing premise

The framework assumes the Formalizer's formal specifications capture all the important meaning of the natural language requirements; if a formal specification silently omits or misstates a behavior, the verification guarantees do not protect the user's actual intent.

Editorial extensions

If this is right

  • Generated code could carry a verification certificate: a program is trustworthy not because the LLM is probable but because model checking and deductive verification have succeeded against an explicit specification.
  • Quality assurance moves upstream: ambiguity, missing constraints, and conflict are addressed in requirements analysis rather than discovered by tests.
  • Every project run through the pipeline yields an aligned triple of requirement specification, formal specification, and verified code, which can be reused to train or fine-tune future agents.
  • Human experts stop reviewing code line by line and instead focus on ambiguous requirements, architecture-model inconsistencies, and verification failures.
  • The two-tier specification style seen in the case study suggests a general recipe: use LTL-style logic for system-level behavior and contract-style annotations for component-level functions.

Reading between the lines

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

  • The real correctness burden in ReDeFo sits with the Formalizer: if specification generation is flawed, both downstream verification passes can succeed while the delivered software fails user intent. A practical next step is to measure formalization quality separately from code quality.
  • The framework could be extended to non-safety-critical domains by relaxing full formal verification to lighter mechanisms such as property-based testing or runtime assertion checking when proof effort is too expensive.
  • If ReDeFo is right that formalization, not code synthesis, is the bottleneck, it would invert the current research emphasis in LLM code generation: more effort should go into requirements-to-specification and less into making single prompts produce perfect code.
  • The claimed 'first' status invites a direct comparison: run the same requirements through a baseline LLM agent without the formalization step and through ReDeFo, then compare verified-correct rate and human-judged satisfaction; the paper does not yet report such a comparison.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 4 minor

Summary. The paper proposes ReDeFo, a multi-agent framework for automated code generation from natural-language requirements. Three agents—Analyst, Formalizer, and Coder—are responsible for requirements refinement, formal specification in appropriate formalisms, and verified code generation. Formal verification via model checking (NuSMV) and deductive verification (Frama-C) is applied to architecture models and generated code. A case study on a mode-switching component of a solar-acquisition system is described, and the paper discusses challenges of specification completeness/consistency, code synthesis quality, and practical deployment. The central claim is that ReDeFo provides formal correctness guarantees and is the first multi-agent framework for ACG with such guarantees.

Significance. If implemented and if the specification-intent alignment problem were solved, the core idea of interposing formal specifications as a semantic contract between natural-language requirements and LLM-generated code would be valuable. The three-agent decomposition with distinct knowledge sources is sensible, and the emphasis on acquiring formal-methods knowledge from projects, literature, and experts is a useful contribution to the vision. The paper is also candid in Section IV-A about the completeness and consistency challenge. However, the manuscript contains no implementation, no machine-checked artifacts, no concrete verification outputs, and no evaluation; as a result, its current value is as a position/vision statement rather than a validated framework. The claimed correctness guarantees are materially stronger than what is demonstrated.

major comments (4)
  1. [I and IV-A] The central claim that ReDeFo 'enables rigorous reasoning about correctness' and offers 'formal correctness guarantees' is not supported by the described pipeline. Section III's verification steps (NuSMV against LTL, Frama-C against ACSL) establish only that generated code satisfies the Formalizer's formal specifications. Section IV-A explicitly concedes: 'Even if the code is formally verified against the specification, any mismatch between the specification and the original intent still renders the system incorrect from the user's perspective.' No mechanism in the framework checks that the formal specifications faithfully and completely capture the NLRs; the Formalizer is an LLM-based agent with no completeness guarantee, and the human-in-the-loop review is advisory. As written, the correctness guarantee is conditional on an unverified assumption, so the contribution should be reframed
  2. [III] The case study is described narratively but not demonstrated. The text says 'All the artifacts produced through the pipeline are presented in Figure 2,' yet no concrete LTL formulas, ACSL annotations, C code, NuSMV model, or Frama-C verification output appear in the manuscript. There is also no implementation of the agents. Consequently, the claimed 'potential capabilities' cannot be inspected or reproduced, and the paper provides no evidence that the three-agent pipeline can actually produce verified code. A proof-of-concept with at least one end-to-end artifact set is needed to support the framework's central claim.
  3. [II-A2] The Formalizer's 'consistency assessment' and 'completion of specifications' are listed as key actions, but no concrete method, heuristic, or criterion is provided. Section IV-A identifies completeness and consistency as a key challenge, but the paper does not propose a solution. The cited strategies (e.g., structural checks, behavioral coverage analysis, traceability/consistency verification) are not instantiated for the LLM-based Formalizer. Since validation of the specification against the original intent is the load-bearing step for the correctness claim, leaving this step entirely to unspecified agent behavior is a gap that should be addressed or explicitly scoped out.
  4. [I] The claim that 'to the best of our knowledge, this is the first multi-agent framework for ACG with formal correctness guarantees' is not substantiated. MetaGPT and ChatDev are cited as related multi-agent code generation systems, and there is substantial prior work on NL-to-LTL conversion, LLM autoformalization, and formal verification of LLM-generated code (refs. [15]-[18], [26], [30], [31]). The novelty claim should either be supported with a systematic comparison to existing frameworks or weakened to a position statement.
minor comments (4)
  1. [Abstract] The line 'Index T erms' should read 'Index Terms'.
  2. [II-B1] The statement 'We are confident that LLMs at the heart of agents have already internalized diverse programming paradigms...' is an assumption, not a demonstrated fact. It should be labeled as a design assumption or supported with evidence.
  3. [II] Figure 1 is dense and the flow from knowledge sources to agents to artifacts is hard to parse. Consider redrawing or separating the knowledge-acquisition dimension from the agent workflow.
  4. [III] The phrase 'state diagram1' with a footnote is awkward; the footnote should be integrated into the text or removed.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the verification claim is conditional, not circular, and self-citations are non-load-bearing.

full rationale

ReDeFo is a position/vision paper with no equations, fitted parameters, or quantitative predictions, so the usual reduction-by-construction patterns do not arise. The pipeline's only formal claim is that generated code is verified against the formal specifications produced by the Formalizer (Section III: 'Formal verification is then performed on the architecture model and generated code to guarantee correctness with respect to the specifications.'). That claim is definitionally safe: checking code against a stated specification is exactly what NuSMV/Frama-C do. It does not reduce to its input because the specification is an intermediate artifact, not the output. The paper explicitly disclaims the stronger claim in Section IV-A: 'Even if the code is formally verified against the specification, any mismatch between the specification and the original intent still renders the system incorrect from the user's perspective.' This means the advertised 'correctness guarantees' are conditional on an unverified alignment between NLRs and formal specs; that is an unsupported strength of claim, not a circular derivation. The self-citations ([12], [28], [29]) are used only to motivate the Analyst's refinement actions and knowledge acquisition; they are not load-bearing for the framework's correctness argument. No ansatz is smuggled in via citation, no uniqueness theorem is imported, and no known result is renamed. Accordingly the circularity score is low.

Assumptions & free parameters 0 free parameters · 3 assumptions · 1 invented entities

The paper introduces no numerical free parameters. It relies on several unproven domain assumptions about the feasibility of LLM agents performing reliable formalization and verification, and the sufficiency of verification against assumed-complete specifications. The only invented entity is the framework itself, which has no independent evidence.

assumptions (3)
  • domain assumption Formal verification of generated code against formal specifications is sufficient to guarantee correctness with respect to user requirements.
    The ReDeFo pipeline rests on the premise that verifying code against a formal specification ensures it meets the original intent. This assumes the specification is complete and aligned with the requirements, which the paper itself identifies as a challenge (Section IV-A).
  • domain assumption LLM agents can be effectively augmented with formal-methods knowledge via fine-tuning, CoT, and RAG to produce reliable formal specifications and verified code.
    Section II-B and III assert that knowledge injection enables agents to perform formalization and verification tasks, but no empirical evidence is provided in the paper.
  • domain assumption Real-world software projects can be reverse-engineered to provide aligned requirement-specification-code training data.
    Section II-B.1 proposes extracting formal specifications from source code to train agents, but the paper does not demonstrate this is feasible at scale.
invented entities (1)
  • ReDeFo framework (Analyst, Formalizer, Coder agents)
    purpose: To structure the requirements-to-verified-code pipeline and enable formal correctness guarantees.
    The framework is the paper's core proposal; no implementation or falsifiable predictions are given. The three agents are conceptual roles, not validated software.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision." pith.science (2026). https://pith.science/paper/HEDVAEUV

@misc{pith2026250818675,
  author       = {Pith},
  title        = {Pith review of: Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HEDVAEUV}},
  note         = {Machine review of arXiv:2508.18675}
}
read the original abstract

Automated code generation has long been considered the holy grail of software engineering. The emergence of Large Language Models (LLMs) has catalyzed a revolutionary breakthrough in this area. However, existing methods that only rely on LLMs remain inadequate in the quality of generated code, offering no guarantees of satisfying practical requirements. They lack a systematic strategy for requirements development and modeling. Recently, LLM-based agents typically possess powerful abilities and play an essential role in facilitating the alignment of LLM outputs with user requirements. In this paper, we envision the first multi-agent framework for reliable code generation based on \textsc{re}quirements \textsc{de}velopment and \textsc{fo}rmalization, named \textsc{ReDeFo}. This framework incorporates three agents, highlighting their augmentation with knowledge and techniques of formal methods, into the requirements-to-code generation pipeline to strengthen quality assurance. The core of \textsc{ReDeFo} is the use of formal specifications to bridge the gap between potentially ambiguous natural language requirements and precise executable code. \textsc{ReDeFo} enables rigorous reasoning about correctness, uncovering hidden bugs, and enforcing critical properties throughout the development process. In general, our framework aims to take a promising step toward realizing the long-standing vision of reliable, auto-generated software.

Figures

Figures reproduced from arXiv: 2508.18675 by the authors.

Figure 1
Figure 1. Overview of the proposed framework ReDeFo verification methodologies as well as their respective strengths, limitations, and applicable contexts. For example, using model checking for state-based systems with bounded complexity, or theorem proving for systems requiring high expressiveness and rigor. (2) Mapping strategies from formal specification to code, possibly including language-specific implementation patterns… view at source ↗
Figure 2
Figure 2. Main artifacts of ReDeFo on a practical example III. Case Study In this section, we demonstrate the potential capabilities of ReDeFo through a practical example. The selected case is typ￾ical control software in the safety-critical aerospace domain, which imposes strict constraints on functional correctness, compliance with domain standards, and hardware-dependent operations. The system is named Solar Search (SS), w… view at source ↗

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

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

  1. Semantic-Enhanced Automatic Refinement of Architecture Recovery Results Using LLMs

    cs.SE 2026-07 conditional novelty 6.0 of 10

    SemRef refines existing architecture-recovery outputs with LLMs and dependency analysis, reducing distance to ground truth by 17.72–43.35% RDP across five metrics on 90 recoveries.

Reference graph

Works this paper leans on

47 extracted references · 35 canonical work pages · cited by 1 Pith paper

  1. [12]

    Envisioning intelligent requirements engineering via knowledge-guided multi-agent collabora- tion,

    J. Huang, D. Jin, W. Sun, Y. Liu, and Z. Jin, “Envisioning intelligent requirements engineering via knowledge-guided multi-agent collabora- tion,” in Proceedings of the 40th International Conference on Automated Software Engineering - New Ideas and Emerging Results Track . Seoul, South Korea: IEEE Computer Society, Sun 16 - Thu 20 November 2025, pp. 1–6

    work page 2025

  2. [28]

    Source code summarization in the era of large language models,

    W. Sun, Y. Miao, Y. Li, H. Zhang, C. Fang, Y. Liu, G. Deng, Y. Liu, and Z. Chen, “Source code summarization in the era of large language models,” in Proceedings of the 47th International Conference on Soft- ware Engineering, no. 1. Ottawa, Ontario, Canada: IEEE Computer Society, 27 April-3 May 2025, pp. 419–431

    work page 2025

  3. [29]

    Knowledge-based multi- agent framework for automated software architecture design,

    Y. Zhang, R. Li, P. Liang, W. Sun, and Y. Liu, “Knowledge-based multi- agent framework for automated software architecture design,” in Pro- ceedings of the 33rd ACM International Conference on the Foundations of Software Engineering-Ideas, Visions and Reflections . Trondheim, Norway: ACM, Mon 23 - Fri 27 June 2025, pp. 1–5

    work page 2025

  4. [15]

    Formal specifications from natural language,

    C. Hahn, F. Schmitt, J. J. Tillman, N. Metzger, J. Siber, and B. Finkbeiner, “Formal specifications from natural language,” arXiv preprint arXiv:2206.01962, 2022

    arXiv 2022

  5. [18]

    Autoformalization with large language models,

    Y. Wu, A. Q. Jiang, W. Li, M. Rabe, C. Staats, M. Jamnik, and C. Szegedy, “Autoformalization with large language models,” Advances in Neural Information Processing Systems , vol. 35, pp. 32 353–32 368, 2022

    work page 2022

  6. [26]

    Combining llm code generation with formal specifica- tions and reactive program synthesis,

    W. Murphy, N. Holzer, F. Qiao, L. Cui, R. Rothkopf, N. Koenig, and M. Santolucito, “Combining llm code generation with formal specifica- tions and reactive program synthesis,” arXiv preprint arXiv:2410.19736, 2024

    arXiv 2024

  7. [30]

    Enchanting program specification synthesis by large language models using static analysis and program verification,

    C. Wen, J. Cao, J. Su, Z. Xu, S. Qin, M. He, H. Li, S.-C. Cheung, and C. Tian, “Enchanting program specification synthesis by large language models using static analysis and program verification,” in International Conference on Computer Aided Verification . Springer, 2024, pp. 302– 328

    work page 2024

  8. [31]

    Specgen: Automated generation of formal program specifications via large language models,

    L. Ma, S. Liu, Y. Li, X. Xie, and L. Bu, “Specgen: Automated generation of formal program specifications via large language models,” arXiv preprint arXiv:2401.08807, 2024

    arXiv 2024

Show all 47 references
  1. [1]

    Logic, arithmetic, and automata,

    A. Church, “Logic, arithmetic, and automata,” in Proceedings of the international congress of mathematicians , vol. 1962, 1962, pp. 23–35

    1962

  2. [2]

    Deepseek llm: Scaling open-source language models with longtermism,

    X. Bi, D. Chen, G. Chen, S. Chen, D. Dai, C. Deng, H. Ding, K. Dong, Q. Du, Z. Fu et al., “Deepseek llm: Scaling open-source language models with longtermism,” arXiv preprint arXiv:2401.02954, 2024

    2024 arXiv

  3. [3]

    Gpt-4 technical report,

    J. Achiam, S. Adler, S. Agarwal, L. Ahmad, I. Akkaya, F. L. Aleman, D. Almeida, J. Altenschmidt, S. Altman, S. Anadkat et al. , “Gpt-4 technical report,” arXiv preprint arXiv:2303.08774, 2023

    2023 arXiv

  4. [4]

    A survey on large language models for code generation,

    J. Jiang, F. Wang, J. Shen, S. Kim, and S. Kim, “A survey on large language models for code generation,” arXiv preprint arXiv:2406.00515, 2024

    2024 arXiv

  5. [5]

    Metagpt: Meta programming for multi-agent collaborative framework,

    S. Hong, X. Zheng, J. Chen, Y. Cheng, J. Wang, C. Zhang, Z. Wang, S. K. S. Yau, Z. Lin, L. Zhou et al., “Metagpt: Meta programming for multi-agent collaborative framework,” arXiv preprint arXiv:2308.00352, vol. 3, no. 4, p. 6, 2023

    2023 arXiv

  6. [6]

    Chatdev: Communicative agents for software development,

    C. Qian, W. Liu, H. Liu, N. Chen, Y. Dang, J. Li, C. Yang, W. Chen, Y. Su, X. Cong et al. , “Chatdev: Communicative agents for software development,” arXiv preprint arXiv:2307.07924, 2023

    2023 arXiv

  7. [7]

    Requirements are all you need: From requirements to code with llms,

    B. Wei, “Requirements are all you need: From requirements to code with llms,” in 2024 IEEE 32nd International Requirements Engineering Conference (RE). IEEE, 2024, pp. 416–422

    2024

  8. [8]

    Is your code generated by chatgpt really correct? rigorous evaluation of large language models for code generation,

    J. Liu, C. S. Xia, Y. Wang, and L. Zhang, “Is your code generated by chatgpt really correct? rigorous evaluation of large language models for code generation,” Advances in Neural Information Processing Systems , vol. 36, pp. 21 558–21 572, 2023

    2023

  9. [9]

    Formal methods: State of the art and future directions,

    E. M. Clarke and J. M. Wing, “Formal methods: State of the art and future directions,” ACM Computing Surveys (CSUR) , vol. 28, no. 4, pp. 626–643, 1996

    1996

  10. [10]

    Formal methods: Practice and experience,

    J. Woodcock, P. G. Larsen, J. Bicarregui, and J. Fitzgerald, “Formal methods: Practice and experience,” ACM computing surveys (CSUR) , vol. 41, no. 4, pp. 1–36, 2009

    2009

  11. [11]

    Nissanke, Formal Specification: Techniques and Applications

    N. Nissanke, Formal Specification: Techniques and Applications . Springer Science & Business Media, 2012

    2012

  12. [13]

    Elicitron: An llm agent-based simulation framework for design require- ments elicitation,

    M. Ataei, H. Cheong, D. Grandi, Y. Wang, N. Morris, and A. Tessier, “Elicitron: An llm agent-based simulation framework for design require- ments elicitation,” arXiv preprint arXiv:2404.16045, 2024

    2024 arXiv

  13. [14]

    P. A. Laplante and M. Kassab, Requirements engineering for software and systems. Auerbach Publications, 2022

    2022

  14. [16]

    NL2LTL – a python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas,

    F. Fuggitti and T. Chakraborti, “NL2LTL – a python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas,” in AAAI, 2023, system Demonstration

    2023

  15. [17]

    From informal to formal–incorporating and evaluating llms on natural language requirements to verifiable formal proofs,

    J. Cao, Y. Lu, M. Li, H. Ma, H. Li, M. He, C. Wen, L. Sun, H. Zhang, S. Qin et al. , “From informal to formal–incorporating and evaluating llms on natural language requirements to verifiable formal proofs,” arXiv preprint arXiv:2501.16207, 2025

    2025 arXiv

  16. [19]

    Baier and J.-P

    C. Baier and J.-P. Katoen, Principles of model checking . MIT press, 2008

    2008

  17. [20]

    D. W. Loveland, Automated theorem proving: A logical basis. Elsevier, 2016

    2016

  18. [21]

    Introduction to static analysis,

    X. Rival and K. Yi, “Introduction to static analysis,” 2020

    2020

  19. [22]

    Software verification using k-induction,

    A. F. Donaldson, L. Haller, D. Kroening, and P. R¨ ummer, “Software verification using k-induction,” in Static Analysis: 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceed- ings 18. Springer, 2011, pp. 351–368

    2011

  20. [23]

    An axiomatic basis for computer programming,

    C. A. R. Hoare, “An axiomatic basis for computer programming,” Communications of the ACM , vol. 12, no. 10, pp. 576–580, 1969

    1969

  21. [24]

    Rescher and A

    N. Rescher and A. Urquhart, Temporal logic . Springer Science & Business Media, 2012, vol. 3

    2012

  22. [25]

    Completeness and consistency of tabular requirements: An smt-based verification approach,

    C. Menghi, E. Balai, D. Valovcin, C. Sticksel, and A. Rajhans, “Completeness and consistency of tabular requirements: An smt-based verification approach,” IEEE Trans. Software Eng. , vol. 51, no. 2, pp. 595–620, 2025. [Online]. Available: https://doi.org/10.1109/TSE.2025.3530820

    2025

  23. [27]

    Synthe- sis of reactive (1) designs,

    R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y. Sa’ar, “Synthe- sis of reactive (1) designs,” Journal of Computer and System Sciences , vol. 78, no. 3, pp. 911–938, 2012

    2012

  24. [32]

    The specification language tla+,

    S. Merz, “The specification language tla+,” Logics of specification languages, pp. 401–451, 2008

    2008

  25. [33]

    Baudin, J.-C

    P. Baudin, J.-C. Filli ˆatre, C. March ´e, B. Monate, Y. Moy, and V. Prevosto, ACSL: ANSI/ISO C Specification Language . [Online]. Available: http://frama-c.com/download/acsl.pdf

  26. [34]

    Bertot and P

    Y. Bertot and P. Cast ´eran, Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media, 2013

    2013

  27. [35]

    Cousot, Principles of abstract interpretation

    P. Cousot, Principles of abstract interpretation . MIT Press, 2021

    2021

  28. [36]

    Satisfiability modulo theories,

    C. Barrett and C. Tinelli, “Satisfiability modulo theories,” Handbook of model checking, pp. 305–343, 2018

    2018

  29. [37]

    The nuxmv symbolic model checker,

    R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta, “The nuxmv symbolic model checker,” inComputer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vien...

    2014

  30. [38]

    Correnson, P

    L. Correnson, P. Cuoq, F. Kirchner, A. Maroneze, V. Prevosto, A. Puccetti, J. Signoles, and B. Yakobowski, Frama-C User Manual. [Online]. Available: http://frama-c.com/download/frama-c- user-manual.pdf

  31. [39]

    Cpachecker: A tool for configurable software verification,

    D. Beyer and M. E. Keremoglu, “Cpachecker: A tool for configurable software verification,” in Computer Aided Verification: 23rd Interna- tional Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23. Springer, 2011, pp. 184–190

    2011

  32. [40]

    Z3: An efficient smt solver,

    L. De Moura and N. Bjørner, “Z3: An efficient smt solver,” in Inter- national conference on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 2008, pp. 337–340

    2008

  33. [41]

    Lora: Low-rank adaptation of large language models

    E. J. Hu, Y. Shen, P. Wallis, Z. Allen-Zhu, Y. Li, S. Wang, L. Wang, W. Chen et al., “Lora: Low-rank adaptation of large language models.” ICLR, vol. 1, no. 2, p. 3, 2022

    2022

  34. [42]

    Chain-of-thought prompting elicits reasoning in large language models,

    J. Wei, X. Wang, D. Schuurmans, M. Bosma, F. Xia, E. Chi, Q. V. Le, D. Zhou et al. , “Chain-of-thought prompting elicits reasoning in large language models,” Advances in neural information processing systems , vol. 35, pp. 24 824–24 837, 2022

    2022

  35. [43]

    Retrieval- augmented generation for knowledge-intensive nlp tasks,

    P. Lewis, E. Perez, A. Piktus, F. Petroni, V. Karpukhin, N. Goyal, H. K¨ uttler, M. Lewis, W.-t. Yih, T. Rockt ¨aschel et al. , “Retrieval- augmented generation for knowledge-intensive nlp tasks,” Advances in neural information processing systems , vol. 33, pp. 9459–9474, 2020

    2020

  36. [44]

    The temporal logic of programs,

    A. Pnueli, “The temporal logic of programs,” in 18th annual symposium on foundations of computer science (sfcs 1977) . ieee, 1977, pp. 46–57

    1977

  37. [45]

    Acsl: Ansi/iso c specification,

    P. Baudin, J.-C. Filli ˆatre, C. March´e, B. Monate, Y. Moy, and V. Prevosto, “Acsl: Ansi/iso c specification,” URL https://frama-c. com/html/acsl. html, 2021

    2021

  38. [46]

    Nusmv 2: An opensource tool for symbolic model checking,

    A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella, “Nusmv 2: An opensource tool for symbolic model checking,” in Computer Aided Verification: 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27–31, 20...

    2002

  39. [47]

    Frama-c: A software analysis perspective,

    F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, “Frama-c: A software analysis perspective,” Formal aspects of comput- ing, vol. 27, no. 3, pp. 573–609, 2015

    2015

Pith tools

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