Pith. sign in

REVIEW 3 major objections 5 minor 2 cited by

Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software

T0 review · 3 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read A feasibility study shows LLMs can turn specifications into formally verified embedded C code without iterative repair, though only in two of three industrial cases.

desk verdict A real but modest feasibility study; the ghost-variable conversion in all cases means the Frama-C proofs target an altered specification, so the headline claim needs reining in. read the letter →

arxiv 2411.13269 v1 pith:J5BO4DNY submitted 2024-11-20 cs.SE cs.AI

Minal Suresh Patil , Gustav Ung , Mattias Nyberg This is my paper · ORCID
classification cs.SEcs.AI
keywords CodeGenerationFormalverificationLargeLanguageModelsAutomatedSoftwareEngineeringACSLembeddeddeductivespec2code
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 tries to establish that off-the-shelf large language models, guided only by specifications and checked by a compiler and a deductive verifier, can generate embedded C code of industrial quality. It introduces spec2code, a framework in which an LLM produces code from formal ACSL contracts and natural-language requirements, and critics (a compiler and a verification tool) assess the output. A deliberately weak instantiation of the framework, with no iterative backprompting and no fine-tuning, was applied to three production modules for truck electronics. The generated code compiled in all three case studies, and Frama-C formally verified the code against its ACSL specifications for at least one combination of specification types in two of the three modules. The paper argues this makes it plausible that specification-driven code generation can eventually shift the bottleneck of safety-critical software development from coding to the writing of complete formal specifications.

What carries the argument

The load-bearing object is spec2code, a framework that wraps an LLM in a loop of critics: a verification engineer writes specifications in natural language and in ACSL, a prompt template (built on Zero-shot-CoT, i.e. the instruction 'Let's think step by step') asks the model to complete a given C function from the module interface, and the output must first survive compilation by GCC and then be checked by Frama-C's WP plugin against the ACSL contract. In the full framework the critics' feedback feeds iterative backprompting, supervised fine-tuning, and preference optimization; the feasibility study removes all of those and keeps only one-shot generation followed by the critics, which allows the experiment to isolate whether the LLM itself can carry the specification-to-code step. A notable detail is that ghost variables in the ACSL contracts were converted into ordinary concrete variables in the prompt, because the models tended to misuse them; this conversion is part of what makes the formal verification go through.

What would settle it

Have a second engineer independently translate the natural-language requirements of the three modules into ACSL specifications without seeing the original code or the paper's contracts, then rerun the same prompts; if any of the newly generated programs fails to compile or fails Frama-C verification, the original verified results were carried by the particular hand-written specifications rather than by the method itself.

Watch

Extended reading notes

Core claim

The central discovery is a positive feasibility result for the 'minimalist' version of spec2code: without iterative backprompting and without fine-tuning, a single zero-shot chain-of-thought prompt fed with ACSL specifications, high-level natural-language specifications, low-level natural-language specifications, or their combinations produced C code that compiled with GCC in all three case studies (Steering Fluid Level Detection, Brake Light Activation, Power Steering Backup). Using Frama-C's weakest-precondition plugin, the paper reports fully proved verification goals for several specification combinations in the Brake Light and Power Steering modules, and partial proof obligations elsewhere, with GPT-4-turbo more consistently successful than GPT-3.5. The paper is careful to note that program-equivalence checking against the original hand-written reference programs did not succeed in any case; manual inspection attributes this to ghost variables being realized as concrete variables in generated code and to unspecified behavior, not necessarily to functional deviation. It also reports that every compilable generated program adhered to the 'power of 10' rules for safety-critical code and generated no compiler warnings. The conclusion the authors draw is that formally correct code can be generated from specifications alone, at least for small, single-function modules, and that the main remaining condition is completeness of the specifications.

Load-bearing premise

The central claim depends on the assumption that the hand-written ACSL specifications fully and faithfully capture what the original Scania modules are supposed to do, since the formal verification only proves the generated code against those specifications, not against the original code's intent.

Editorial extensions

If this is right

  • If one-shot, specification-only generation can be formally verified on small modules, the same pipeline is a candidate for larger modules once iterative backprompting and fine-tuning are added, which the paper explicitly plans as future work.
  • The success of the minimalist instantiation depends on the completeness of the ACSL specifications; the paper concludes that complete specifications are rare in real industrial development, so the practical gain of LLM-based coding must be weighed against the extra effort of writing complete specs.
  • High-level natural-language specifications alone produced the weakest verification results, indicating that formal or low-level specifications are needed for reliable code generation.
  • Because all generated programs passed the 'power of 10' rules and compiled with no warnings, the approach is at least compatible with the coding standards used in safety-critical automotive software.

Reading between the lines

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

  • An implication the authors leave implicit: if the bottleneck becomes specification completeness, then the cost of formalizing requirements may come to dominate the software life cycle, so the economic case for spec2code will hinge on whether spec-writing effort is smaller than the coding effort it replaces.
  • The same verification-backed loop could transfer to other safety-critical domains (e.g., avionics, medical devices) by swapping Frama-C for an equivalent deductive verifier, since the framework does not depend on automotive-specific features.
  • Because equivalence checking against the original code failed in every case, the paper's 'formally correct' means 'correct with respect to the hand-derived ACSL contract,' not 'behaviorally identical to the original module'; a stronger test would compare against a second, independently written specification.
  • The pass@1 evaluation under temperature 0.8 likely understates what the pipeline could achieve: sampling several candidates and verifying each would probably raise the success rate, which the paper notes as future work with pass@k.
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

3 major / 5 minor

Summary. The paper proposes spec2code, a framework that combines LLM-based code generation with software verifiers and other critics in an iterative refinement loop, and then evaluates a minimalist instantiation of it on three industrial automotive modules from Scania (SFLD, BRAK, STEE). In the feasibility study, gpt-3.5 and gpt-4-turbo are prompted with combinations of high-level natural language, low-level natural language, and ACSL formal specifications; the generated C code is compiled with GCC, verified with Frama-C WP using Z3 and Alt-Ergo, checked for semantic equivalence with diffkemp against reference implementations, and manually assessed against the 'power of 10' rules. The results show that compilable code is produced for many specification combinations, and that fully verified code (all proof goals proved) is obtained for some combinations in two of the three case studies, but diffkemp equivalence failed in every case. The paper concludes that formally correct code can be generated from specifications without iterative backprompting or fine-tuning, while acknowledging that correctness is relative to the supplied specifications.

Significance. If substantiated, the result is a meaningful feasibility data point: it suggests that off-the-shelf LLMs can generate code that passes machine-checked formal verification from formal specifications in a single generation step, without iterative prompting or fine-tuning, in a safety-critical automotive context. The study has several strengths: the use of real, proprietary Scania modules avoids the well-known training-data leakage threat; the verification results are produced by external tools (Frama-C WP with Z3 and Alt-Ergo) rather than by the LLM itself; and the paper is transparent about important limitations. The spec2code framework itself is a useful conceptual contribution, though its general formulation is largely an adaptation of the LLM-Modulo framework. The significance is substantially tempered, however, by two issues: the ACSL specifications used in the experiments were altered (ghost variables converted to concrete variables), so the verification is not against the original hand-derived specifications; and the semantic equivalence checks with the reference programs failed in all cases.

major comments (3)
  1. [Section 7 (Ghost variables)] The conversion of ghost variables to concrete variables, stated in the 'Ghost variables' paragraph, changes the verification target. The Frama-C proofs reported in Tables 1-3 are for these converted specifications, not for the original hand-derived ACSL specifications described in Section 4.2. Because the generated programs are required to assign concrete global variables that the reference programs keep local, the proof does not establish that the generated code satisfies the original ACSL specifications. The authors themselves report in the same section that diffkemp equivalence fails in all cases, partly for this reason. Therefore the conclusion in Section 8 that 'formally correct code' was generated is only justified with respect to the modified specifications, and the paper does not establish correctness with respect to the intended behavior of the reference modules. The authors should either rerun the verification against the original ghost-variable specifications (for example, using Frama-C's ghost-variable support with appropriate ghost statements), or provide a rigorous argument and evidence that the conversion preserves the intended functional behavior.
  2. [Section 6 and Section 8] The term 'formally verified' is used without an explicit operational criterion. The 'Verified (Proved Goals)' columns in Tables 1-3 report ratios such as 33/33, 41/50, and 8/8, but the text does not state that a row is considered verified only when all proof goals are discharged, nor does it identify which specific rows support the conclusion that formal verification was achieved 'for some combination of specifications, in two of the three case studies.' A reader cannot unambiguously map that claim to the data; for example, BRAK shows 30/30 for HLNL+LLNL (a combination that includes no formal ACSL), while STEE shows 8/8 for several ACSL-inclusive combinations. Please define the verification criterion explicitly and list the exact (model, specification) combinations that are fully verified, and relate those to the conclusion.
  3. [Section 7 (Equivalence checking) and Section 8] The paper reports that the program equivalence check failed for every generated program, and attributes this to unspecified behavior and the ghost-variable conversion. However, it does not provide a concrete analysis of whether the observed semantic deviations between generated and reference programs are benign (e.g., only additional writes to formerly ghost variables) or whether they could correspond to genuine functional differences. Without such an analysis, the statement in Section 8 that the generated code is of 'industrial quality' and 'could be hypothetically integrated in the Scania production code' is not supported by the presented evidence. At most, the study shows that generated code can satisfy the (modified) ACSL specifications; it does not show that the code would behave equivalently to the original production modules.
minor comments (5)
  1. [Section 4.2] The process of deriving ACSL specifications by hand from natural language specifications is a load-bearing step for the whole study, yet it is described in a single sentence. A short description of the derivation method, the expertise involved, and any consistency checks would help readers judge the quality and completeness of the formal specifications.
  2. [Section 5.2] The LLM hyperparameters are reported, but there is no sensitivity analysis for temperature or other parameters. Since the study relies on a single pass@1 output per configuration, the results may be sensitive to the chosen temperature (0.8); a small-scale variation study or a justification based on prior work would strengthen the comparisons.
  3. [Tables 1-3] The column header 'Verified (Proved Goals)' mixes two pieces of information: the number of proved goals out of the total, and whether equivalence was shown. Consider splitting this into separate columns, e.g., 'Proved goals' and 'Equivalence', with a clear note on what 'Not Eq' means (equivalence could not be shown, not necessarily that the programs are inequivalent).
  4. [Section 7] The term 'pass@1' is used in the LLM comparison paragraph but not defined; please define it or replace it with a standard metric name (e.g., 'first-attempt success').
  5. [Appendix A] The prompt template is informative, but it is unclear how the ACSL specifications (including any ghost variables) are inserted into the prompt. Clarify the exact placement and formatting of ACSL annotations relative to the C header and function signature, since this directly affects the LLM's behavior.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: specs are hand-written inputs; Frama-C checks are external and not fitted; ghost-variable conversion is a validity limitation, not a circular reduction.

full rationale

The derivation chain is not circular. The hand-derived ACSL specifications (Section 4.2: 'From these natural language specifications, the ACSL specifications were derived by hand.') are inputs supplied before code generation, not outputs fitted to the generated code or to the verification results. No parameter is fitted, no prediction is obtained from data, and no uniqueness theorem from the authors' prior work is used to force a choice. The Frama-C proofs are external machine-checked checks (Z3/Alt-Ergo) of the generated code against the given ACSL contract; the diffkemp equivalence check, though it failed in all cases, is an independent comparison against reference programs, and the paper reports that failure. The two concerns raised in the paper are limitations, not circularities. First, the ghost-variable conversion (Section 7: 'in all our case studies, we converted the ghost variables in the specification to concrete variables') changes the verified property, so the proof establishes satisfaction of the converted specification rather than the original ghost-variable specification; but the converted specification is not defined in terms of the generated code, and proving code against it still requires nontrivial verification work. Second, the conclusion explicitly disclaims behavioral correctness: 'the correctness of the generated code is with respect to the specifications only.' The only self-citation, [34] for the STEE module, is contextual and not load-bearing; no central claim depends on it. Therefore the paper's empirical feasibility claim does not reduce by construction to its own inputs.

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

The central claim rests on the fidelity of the hand-written ACSL specs and the soundness of Frama-C. The LLM hyperparameters are chosen by hand and are listed as free parameters. No invented entities are introduced.

free parameters (5)
  • LLM temperature = 0.8
    Set to introduce controlled randomness for diverse output (Section 5.2).
  • presence penalty = 0.5
    LLM generation parameter (Section 5.2).
  • frequency penalty = 1
    LLM generation parameter (Section 5.2).
  • max_tokens = 4096
    LLM generation parameter (Section 5.2).
  • top_p = 1
    LLM generation parameter (Section 5.2).
assumptions (5)
  • domain assumption Frama-C WP with Z3 and Alt-Ergo soundly checks ACSL specifications.
    Used for the functional correctness evaluation (Section 5.4).
  • domain assumption The hand-derived ACSL specifications accurately represent the intended functional behavior of the Scania modules.
    The specs are the yardstick for correctness; if they are wrong, verification proves nothing (Sections 4.2 and 8).
  • domain assumption The original Scania code is correct and can be used as a reference for equivalence.
    Used as reference in diffkemp equivalence checking (Section 5.4).
  • domain assumption The LLM API calls return code that is representative of the models' outputs.
    The study assumes no API anomalies; randomness is controlled only by temperature (Section 5.2).
  • ad hoc to paper Converting ghost variables to concrete variables preserves the intended behavior.
    The authors converted ghost variables in all case studies to help compile successfully (Section 7).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software." pith.science (2026). https://pith.science/paper/J5BO4DNY

@misc{pith2026241113269,
  author       = {Pith},
  title        = {Pith review of: Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/J5BO4DNY}},
  note         = {Machine review of arXiv:2411.13269}
}
read the original abstract

The paper studies how code generation by LLMs can be combined with formal verification to produce critical embedded software. The first contribution is a general framework, spec2code, in which LLMs are combined with different types of critics that produce feedback for iterative backprompting and fine-tuning. The second contribution presents a first feasibility study, where a minimalistic instantiation of spec2code, without iterative backprompting and fine-tuning, is empirically evaluated using three industrial case studies from the heavy vehicle manufacturer Scania. The goal is to automatically generate industrial-quality code from specifications only. Different combinations of formal ACSL specifications and natural language specifications are explored. The results indicate that formally correct code can be generated even without the application of iterative backprompting and fine-tuning.

Figures

Figures reproduced from arXiv: 2411.13269 by the authors.

Figure 1
Figure 1. Overview of spec2code framework The paper is organized as follows. In Section 2, background information on deductive verification of C programs and LLMs are presented. Then, in Section 3, we present the first contribution, i.e. the spec2code framework. Section 4, 5, and 6 then describe the second contribution, i.e. the case study on using the minimalist instantiation of the spec2code framework applied to real indust… view at source ↗
Figure 2
Figure 2. ECU System architecture All case study modules in this study are written in C [15], and are developed according to internal coding guidelines largely identical to those of MISRA￾C [23]. The modules are executed in two of several Electronic Control Units (ECUs) in the embedded system of Scania trucks. Each ECU has a static sched￾uler which repeatedly calls the main entry point of each application module once every 10… view at source ↗
Figure 3
Figure 3. Overview of the minimalist version of spec2code framework As shown in [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

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

  1. VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models

    cs.SE 2024-11 conditional novelty 6.0 of 10

    VeCoGen automatically generates and formally verifies loop-free C functions from ACSL and natural language specifications, solving 13 of 15 Codeforces problems with its default model.

  2. Survey of GenAI for Automotive Software Development: From Requirements to Executable Code

    cs.SE 2025-07 conditional novelty 3.0 of 10

    A review of roughly 60 papers and 9 industry respondents finds GPT-family models dominate automotive code generation while requirements handling lags due to confidentiality constraints.

Reference graph

Works this paper leans on

41 extracted references · 22 canonical work pages · cited by 2 Pith papers

  1. [1]

    Lecture notes in computer science 10001 (2016)

    Ahrendt, W., Beckert, B., Bubel, R., H¨ ahnle, R., Schmitt, P.H., Ulbrich, M.: Deductive software verification-the key book. Lecture notes in computer science 10001 (2016)

    work page 2016

  2. [2]

    In: International Symposium on Leverag- ing Applications of Formal Methods

    Ahrendt, W., Gurov, D., Johansson, M., R¨ ummer, P.: Trico—triple co-piloting of implementation, specification and tests. In: International Symposium on Leverag- ing Applications of Formal Methods. pp. 174–187. Springer (2022)

    work page 2022

  3. [3]

    CEA LIST, Inria, https://www.frama-c.com/download/ frama-c-wp-manual.pdf

    Baudin, P., Bobot, F., Correnson, L., Dargaye, Z., Blanchard, A.: WP Plug-in Manual. CEA LIST, Inria, https://www.frama-c.com/download/ frama-c-wp-manual.pdf

    work page

  4. [4]

    URL https://frama-c

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

    work page 2021

  5. [5]

    arXiv preprint arXiv:2107.03374 (2021)

    Chen, M., Tworek, J., Jun, H., Yuan, Q., Pinto, H.P.d.O., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., et al.: Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374 (2021)

    arXiv 2021

  6. [6]

    In: SMT Workshop: International Workshop on Satisfiability Modulo Theories (2018)

    Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-ergo 2.2. In: SMT Workshop: International Workshop on Satisfiability Modulo Theories (2018)

    2018

  7. [7]

    CEA LIST, Inria, http:// frama-c.com/download/frama-c-user-manual.pdf

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

    work page

  8. [8]

    In: International Conference on Computer Aided Verification

    Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., Trippel, C.: nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. In: International Conference on Computer Aided Verification. pp. 383–396. Springer (2023)

    2023

Show all 41 references
  1. [9]

    arXiv preprint arXiv:2303.01158 (2023)

    Cosler, M., Schmitt, F., Hahn, C., Finkbeiner, B.: Iterative circuit repair against formal specifications. arXiv preprint arXiv:2303.01158 (2023)

    2023 arXiv

  2. [10]

    In: International conference on Tools and Algorithms for the Construction and Analysis of Systems

    De Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–

  3. [11]

    arXiv preprint arXiv:2003.04218 (2020)

    Hahn, C., Schmitt, F., Kreber, J.U., Rabe, M.N., Finkbeiner, B.: Teaching tem- poral logics to neural networks. arXiv preprint arXiv:2003.04218 (2020)

    2020 arXiv

  4. [12]

    arXiv preprint arXiv:2206.01962 (2022)

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

    2022 arXiv

  5. [13]

    Computing and Software Science: State of the Art and Perspectives pp

    H¨ ahnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. Computing and Software Science: State of the Art and Perspectives pp. 345–373 (2019)

    2019

  6. [14]

    Com- puter 39(6), 95–99 (2006)

    Holzmann, G.J.: The power of 10: Rules for developing safety-critical code. Com- puter 39(6), 95–99 (2006)

    2006

  7. [15]

    International Organization for Standardization: Programming languages—C (1999), ISO/IEC 9899:1999

    1999

  8. [16]

    International Organization for Standardization: Road vehicles controller area net- work (CAN) (2015), ISO 11898-1:2015

    2015

  9. [17]

    arXiv preprint arXiv:2402.01817 (2024)

    Kambhampati, S., Valmeekam, K., Guan, L., Stechly, K., Verma, M., Bhambri, S., Saldyt, L., Murthy, A.: Llms can’t plan, but can help planning in llm-modulo frameworks. arXiv preprint arXiv:2402.01817 (2024)

    2024 arXiv

  10. [18]

    arXiv preprint arXiv:2310.03714 (2023) 18 M.S

    Khattab, O., Singhvi, A., Maheshwari, P., Zhang, Z., Santhanam, K., Vard- hamanan, S., Haq, S., Sharma, A., Joshi, T.T., Moazam, H., et al.: Dspy: Compil- ing declarative language model calls into self-improving pipelines. arXiv preprint arXiv:2310.03714 (2023) 18 M.S. Patil, ...

    2023 arXiv

  11. [19]

    Advances in neural information processing systems 35, 22199–22213 (2022)

    Kojima, T., Gu, S.S., Reid, M., Matsuo, Y., Iwasawa, Y.: Large language models are zero-shot reasoners. Advances in neural information processing systems 35, 22199–22213 (2022)

    2022

  12. [20]

    Information Processing Letters 93(6), 281–288 (2005)

    Leino, K.R.M.: Efficient weakest preconditions. Information Processing Letters 93(6), 281–288 (2005)

    2005

  13. [21]

    Advances in Neural Information Processing Systems 35, 3843–3857 (2022)

    Lewkowycz, A., Andreassen, A., Dohan, D., Dyer, E., Michalewski, H., Ramasesh, V., Slone, A., Anil, C., Schlag, I., Gutman-Solo, T., et al.: Solving quantitative rea- soning problems with language models. Advances in Neural Information Processing Systems 35, 3843–3857 (2022)

    2022

  14. [22]

    In: 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST)

    Mal ´ ık, V., Vojnar, T.: Automatically checking semantic equivalence between ver- sions of large-scale c projects. In: 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST). pp. 329–339. IEEE (2021), https://github. com/diffkemp/diffkemp

    2021

  15. [23]

    MIRA Ltd: MISRA-C:2004 Guidelines for the use of the C language in critical systems (Oct 2004), https://misra.org.uk/misra-c

    2004

  16. [24]

    arXiv preprint arXiv:2306.09896 (2023)

    Olausson, T.X., Inala, J.P., Wang, C., Gao, J., Solar-Lezama, A.: Demystifying gpt self-repair for code generation. arXiv preprint arXiv:2306.09896 (2023)

    2023 arXiv

  17. [25]

    https://www.openai.com (2022), accessed: 25/04/2024

    OpenAI: gpt-3.5-turbo-0125. https://www.openai.com (2022), accessed: 25/04/2024

    2022

  18. [26]

    https://www.openai.com (2023), accessed: 25/04/2024

    OpenAI: gpt-4-turbo. https://www.openai.com (2023), accessed: 25/04/2024

    2023

  19. [27]

    Advances in neural information processing sys- tems 35, 27730–27744 (2022)

    Ouyang, L., Wu, J., Jiang, X., Almeida, D., Wainwright, C., Mishkin, P., Zhang, C., Agarwal, S., Slama, K., Ray, A., et al.: Training language models to follow instructions with human feedback. Advances in neural information processing sys- tems 35, 27730–27744 (2022)

    2022

  20. [28]

    Advances in Neural Information Processing Systems 36 (2024)

    Rafailov, R., Sharma, A., Mitchell, E., Manning, C.D., Ermon, S., Finn, C.: Direct preference optimization: Your language model is secretly a reward model. Advances in Neural Information Processing Systems 36 (2024)

    2024

  21. [29]

    In: Proceedings of the 28th International Conference on Intelligent User Interfaces

    Ross, S.I., Martinez, F., Houde, S., Muller, M., Weisz, J.D.: The programmer’s assistant: Conversational interaction with a large language model for software de- velopment. In: Proceedings of the 28th International Conference on Intelligent User Interfaces. pp. 491–514 (2023)

    2023

  22. [30]

    IEEE Transactions on Soft- ware Engineering (2023)

    Sch¨ afer, M., Nadi, S., Eghbali, A., Tip, F.: An empirical evaluation of using large language models for automated unit test generation. IEEE Transactions on Soft- ware Engineering (2023)

    2023

  23. [31]

    arXiv preprint arXiv:2210.03057 (2022)

    Shi, F., Suzgun, M., Freitag, M., Wang, X., Srivats, S., Vosoughi, S., Chung, H.W., Tay, Y., Ruder, S., Zhou, D., et al.: Language models are multilingual chain-of- thought reasoners. arXiv preprint arXiv:2210.03057 (2022)

    2022 arXiv

  24. [32]

    Geneva, Switzerland (2018)

    for Standardization (ISO), I.O.: Iso 26262-1: 2018–road vehicles—functional safety. Geneva, Switzerland (2018)

    2018

  25. [33]

    arXiv preprint arXiv:2403.08937 (2024)

    Tambon, F., Dakhel, A.M., Nikanjam, A., Khomh, F., Desmarais, M.C., Antoniol, G.: Bugs in large language models generated code. arXiv preprint arXiv:2403.08937 (2024)

    2024 arXiv

  26. [34]

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

    Ung, G., Amilon, J., Gurov, D., Lidstr¨ om, C., Nyberg, M., Palmskog, K.: Post- hoc formal verification of automotive software with informal requirements: An experience report. In: Accepted at 2024 IEEE 32nd International Requirements Engineering Conference (RE). IEEE (2024)

    2024

  27. [35]

    experience: Evalu- ating the usability of code generation tools powered by large language models

    Vaithilingam, P., Zhang, T., Glassman, E.L.: Expectation vs. experience: Evalu- ating the usability of code generation tools powered by large language models. In: Chi conference on human factors in computing systems extended abstracts. pp. 1–7 (2022) Title Suppressed Due to Ex...

    2022

  28. [36]

    Advances in neural information pro- cessing systems 30 (2017)

    Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A.N., Kaiser, L., Polosukhin, I.: Attention is all you need. Advances in neural information pro- cessing systems 30 (2017)

    2017

  29. [37]

    arXiv preprint arXiv:2212.10001 (2022)

    Wang, B., Min, S., Deng, X., Shen, J., Wu, Y., Zettlemoyer, L., Sun, H.: Towards understanding chain-of-thought prompting: An empirical study of what matters. arXiv preprint arXiv:2212.10001 (2022)

    2022 arXiv

  30. [38]

    arXiv preprint arXiv:2302.10205 (2023)

    Wei, X., Cui, X., Cheng, N., Wang, X., Zhang, X., Huang, S., Xie, P., Xu, J., Chen, Y., Zhang, M., et al.: Zero-shot information extraction via chatting with chatgpt. arXiv preprint arXiv:2302.10205 (2023)

    2023 arXiv

  31. [39]

    https://en.wikipedia.org/w/index.php?title=Assertion_ (software_development)&oldid=1179241560 (2023), [Online; accessed 27-May- 2024]

    Wikipedia contributors: Assertion (software development) — Wikipedia, the free encyclopedia. https://en.wikipedia.org/w/index.php?title=Assertion_ (software_development)&oldid=1179241560 (2023), [Online; accessed 27-May- 2024]

    2023

  32. [40]

    arXiv preprint arXiv:2406.07496 (2024)

    Yuksekgonul, M., Bianchi, F., Boen, J., Liu, S., Huang, Z., Guestrin, C., Zou, J.: Textgrad: Automatic” differentiation” via text. arXiv preprint arXiv:2406.07496 (2024)

    2024 arXiv

  33. [41]

    In: Proceedings of the AAAI Conference on Artificial Intelligence

    Zhong, L., Wang, Z.: Can llm replace stack overflow? a study on robustness and reliability of large language model code generation. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol. 38, pp. 21841–21849 (2024) 20 M.S. Patil, G. Ung, M. Nyberg Appendix A Pr...

    2024

Pith tools

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