Pith. sign in

REVIEW 4 major objections 5 minor 33 references

CASP: An evaluation dataset for formal verification of C code

T0 review · 4 major / 5 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 This paper builds CASP, a 506-pair benchmark of C code with formally verified ACSL specifications, the largest open dataset of its kind.

desk verdict A genuinely useful dataset, but the LLM-repaired pairs need behavior-preservation evidence before CASP can be trusted as a benchmark. read the letter →

arxiv 2508.18798 v1 pith:KLVER6XT submitted 2025-08-26 cs.FL

Niclas Hertzberg , Merlijn Sevenhuijsen , Liv K{aa}reborn , Anna Lokrantz This is my paper · ORCID
classification cs.FL
keywords datasetformalverificationACSLClanguagebenchmarklargemodelsFrama-Cspecification-implementationpairs
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 aims to solve a missing-piece problem: researchers who want to measure whether LLMs can write formal specifications from C code, or C code from specifications, have had no large, ready-to-use benchmark of verified pairs. The authors claim to fill that gap with CASP: 506 deduplicated C functions, each paired with an ACSL specification, every pair formally verified with Frama-C then manually inspected. They draw the raw material from The Stack v1 and v2, filter 25.7 million deduplicated C files down to 1,180 minimally complete ACSL-annotated files, use an LLM to repair 177 that did not verify, and split the surviving files into standalone function-specification pairs. If the dataset is sound, it turns formal verification itself into a clean pass/fail signal for evaluating code and specification generation, which is the key reason a reader should care.

What carries the argument

The load-bearing mechanism is the three-stage pipeline. Stage one: regex patterns with confidence labels isolate ACSL-annotated C files from The Stack v1/v2, then a 'minimally complete' filter drops files with dependencies beyond the standard library. Stage two: Frama-C's WP plugin converts each function's ACSL contract into proof obligations; the RTE plugin adds runtime-error goals; Z3, Alt-Ergo, and CVC4 must prove all goals within a 60-second timeout and 500,000 steps, and files that fail are sent to Gemini 2.0 Flash for up to seven repair iterations. Stage three: a regex extractor and an LLM extractor independently split each verified file into function-specification pairs, the union is

What would settle it

Re-run the 177 repaired files against their originals: for each pair, build a differential harness that feeds identical inputs to the original and repaired function and compares outputs (or for bounded integer inputs, exhaustively enumerate the domain). If any original-valid input yields a different output, that pair's specification does not describe the original program's behavior, and the claim that CASP pairs are trustworthy verified specifications weakens to 'verified in the repaired copy.' A simpler proxy: inspect the repaired contracts for trivial postconditions (e.g., ensures \true) or

Watch

Extended reading notes

Core claim

The paper's central claim is that CASP is the largest openly available dataset of formally verified C code paired with ACSL specifications, and that it is suitable as a benchmark for LLM-based code and specification generation. The evidence: 506 pairs, each 'minimally complete' (self-contained, standard libraries only), each pair verified by Frama-C's WP and RTE plugins with three SMT solvers, each pair deduplicated and checked manually. The authors also report that the source files span a broader semantic region than previous ACSL datasets, and that LLM repair fixed 177 of 888 initially failing files, a 19.9% success rate. The contribution is as much the pipeline as the dataset: a repeatabl

Load-bearing premise

The load-bearing premise is that the LLM repair step (177 of 469 files) preserves what the original code actually did, so the verified specifications are not vacuous or watered down; the prompt tells Gemini not to change the code's purpose, but the paper reports no check that repaired and original files behave identically.

Editorial extensions

If this is right

  • Specification-to-code and code-to-specification generation can now be benchmarked on 506 verified pairs, with Frama-C verification as an unambiguous success metric.
  • Because each pair is self-contained, evaluation pipelines no longer need a parsing step to extract individual contracts from whole files.
  • The documented 19.9% repair success rate becomes a baseline for measuring progress in automated ACSL repair.
  • The pipeline can be rerun on future versions of The Stack to emit fresh, minimally complete pairs, addressing benchmark contamination.
  • The manual inspection of all pairs makes the dataset usable both to evaluate and to fine-tune models, not just to test them.

Reading between the lines

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

  • I infer that the dataset's strongest test lies outside the paper: comparing the behavior of the 177 LLM-repaired files against the original files they came from, to confirm that repair did not change intended semantics. The paper does not report such a differential test.
  • I infer the benchmark will be most informative if split into a public and a private held-out portion, since The Stack is already used in model training and some CASP functions may have been seen during pretraining.
  • The same three-stage pipeline should transfer to other contract languages (for example VeriFast or SPARK), yielding comparable cross-language benchmarks; the paper's regex/tooling choices are language-specific but the architecture is general.
  • A testable extension: measure whether verified LLM-generated specifications are actually useful specifications, e.g., by recording how many proof goals they prove on a fixed corpus of implementations compared to the original human-written specs.
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 / 5 minor

Summary. The paper introduces CASP, a benchmark dataset of 506 C-code/ACSL-specification pairs. The dataset is built by filtering C files from The Stack v1 and v2 for ACSL annotations, keeping only files with no external dependencies beyond standard libraries, and then verifying these files with Frama-C (WP and RTE plugins, with explicit versions: Frama-C 30.0, Z3 4.8.12, Alt-Ergo 2.6.0, CVC4 1.8). Files that do not verify are sent to Gemini 2.0 Flash for repair, with up to seven iterations, and the surviving verified files are then split into standalone function/specification pairs by a regex pipeline and an LLM pipeline, followed by manual post-fixing of remaining unverified pairs, deduplication, and a one-line filter, yielding 506 pairs. The authors claim this is the largest openly available dataset of its kind and state that a manual inspection confirms the correctness of every pair.

Significance. If the verification and curation claims hold, CASP is a useful resource for benchmarking LLMs on specification-to-code and code-to-specification generation, and for training models on formally verified C code. The paper provides exact tool versions and a clearly described pipeline, and the dataset is publicly released on Hugging Face, which is a strength. The diversity analysis against prior datasets (t-SNE, nearest-neighbor distances) is a reasonable post-hoc check. However, the value of the dataset critically depends on two unverified assumptions: (1) the LLM-repaired files preserve the original code's intended behavior, and (2) the claimed manual inspection of every pair was actually performed and is reliable. These points are load-bearing because 177 of the 469 verified source files (37.7%) were modified by Gemini, and because the manual-inspection claim is the only stated safeguard against vacuous or semantically weakened specifications.

major comments (4)
  1. [Section 5.1, Table 4, Appendix B] The repair process modifies 177 of 469 verified source files, yet no protocol establishes that the LLM's changes preserve the original code's behavior. The prompt (Appendix B) instructs Gemini to avoid altering C code 'unless absolutely necessary' and not to 'alter the purpose of the original code', but this is an instruction, not a check. Without differential testing, manual audit of all modified files, or a released diff log, a pair can pass Frama-C while the implementation no longer matches the original author's intent, or while the contract has been weakened to become trivially provable. Since this affects 37.7% of the source files, the central claim that CASP contains verified specification-implementation pairs is not yet substantiated. I recommend adding a behavior-preservation check (e.g., running the original and repaired versions on a shared test suite where feasible, or a manua
  2. [Abstract, Section 5, Section 6] The abstract and Section 5/6 claim that 'a manual inspection is conducted to confirm the correctness of every pair,' but the body only describes manual post-fixing of remaining unverified pairs in Section 6.2. No inspection protocol, criteria for 'correctness,' number of inspectors, or outcomes are reported. This makes the quality guarantee unverifiable. If the manual inspection was performed, the paper should describe it in detail (what was checked, by whom, with what agreement). If not, the claim should be removed or downgraded, and the dataset should be presented as automatically verified rather than human-validated.
  3. [Section 6.2, dataset artifacts] The pair-creation step says 'any remaining unverified pairs were manually post-fixed,' but no record is given of what those changes were, which pairs were affected, or whether the post-fixing altered code, specifications, or both. Additionally, the paper does not provide per-pair verification logs or proof certificates, so a user cannot independently confirm that all 506 pairs indeed verify under the stated Frama-C configuration. I recommend releasing a manifest with each pair's original source file, the extraction pipeline used, the verification status before and after any post-fixing, and the Frama-C WP/RTE logs (or at least the list of proof obligations and their outcomes). This is standard for dataset papers of this kind and would materially strengthen reproducibility.
  4. [Section 3.1, Table 1] There is a numerical inconsistency: Section 3.1 states The Stack v1 contains 'approximately 546 million files,' while Table 1 reports '5.46M' files. This discrepancy affects the reported scale of the source data and should be corrected.
minor comments (5)
  1. [Section 8.2] The statement that 'approximately 35 CASP source files are very similar to some other file' lacks a definition of 'very similar.' Specify the distance threshold used in the nearest-neighbor analysis, and consider reporting the distribution of similarity scores for these cases.
  2. [Section 7.1] The embedding analysis truncates code samples longer than 4096 tokens (CodexEmbed's context limit). Since some CASP source files are longer, the t-SNE and nearest-neighbor plots may misrepresent those samples. A sentence noting this and its potential effect would improve clarity.
  3. [Figure 2] The pipeline diagram is dense and the text labels for the 'Repair Files' and 'LLM-based Separation' branches are difficult to follow. Consider simplifying the figure or adding numbered steps that correspond directly to the section headings.
  4. [Section 4.2] The regex patterns in Appendix A are presented in a table but appear to have formatting issues (e.g., backslashes and spacing). A cleaned presentation using a monospaced listing would aid reproducibility.
  5. [References] Reference [11] ('Inductive Invariant Generation via Abductive Inference') lacks a venue and year. Please complete the bibliographic information.

Circularity Check

0 steps flagged · score 2.0 of 10

No circularity: CASP is constructed by external Frama-C verification of externally sourced code; the only self-citation appears in related work and is not load-bearing.

full rationale

The paper does not derive a mathematical result; it constructs a dataset by filtering The Stack, verifying candidate files with Frama-C's WP and RTE plugins, LLM-repairing non-verifying files, and extracting C/ACSL pairs. None of these steps defines the claimed output in terms of the input: the 506 pairs are checked by an external verification tool against contracts that originate from the source files, not from parameters fitted by the paper. The only self-citation is [26] in Section 3.3 ('Similarly, Sevenhuijsen et al. [26] developed a tool...'), which is related work and is not used to justify CASP's construction, size, or correctness, so it is non-load-bearing. The LLM repair of 177 files (Section 5.1, Table 4) raises a legitimate behavior-preservation and non-vacuity concern, but that is a correctness/quality risk rather than circularity: Frama-C verification is an independent check, and a weakened or semantically drifted contract would be a validity threat, not a definitional reduction of the dataset to its own inputs. Similarly, the abstract's claim that 'a manual inspection is conducted to confirm the correctness of every pair' is not fully evidenced by the protocol descriptions in Sections 5 and 6, but an omitted or underdocumented procedure is not circular reasoning. Thus no circular step is identified; the nonzero score reflects only the presence of the minor, non-load-bearing self-citation.

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

The dataset construction relies on standard tooling assumptions and several choices specific to this paper. The most consequential are the LLM repair fidelity assumption and the unverified manual inspection claim, as they directly affect whether the published pairs truly satisfy their stated specifications.

free parameters (7)
  • WP step limit = 500,000
    Chosen proof search limit for Frama-C WP; affects which goals are provable within the pipeline (Section 5.1).
  • WP timeout per goal = 60 s
    Time limit per proof goal; influences verification success rate (Section 5.1).
  • Maximum repair iterations = 7
    Number of LLM repair attempts for non-verifying files; affects final dataset size (Section 5.1).
  • Minimum function length = strictly > 1 line of code
    Filter to remove trivial one-line functions from dataset (Section 6.2).
  • ACSL detection regex set = Appendix A patterns
    Hand-authored regexes to identify ACSL annotations; determines which files enter the pipeline (Section 4.2).
  • SMT solver set = Z3 4.8.12, Alt-Ergo 2.6.0, CVC4 1.8
    Chosen solvers for proof obligations; a different set may prove more or fewer goals (Section 5.1).
  • Embedding model = CodexEmbed 2B
    Used for semantic similarity analysis; choice affects the diversity claims (Section 7.1).
assumptions (7)
  • domain assumption Frama-C WP and RTE plugins are sound for the C semantics they target.
    The claim that all pairs are formally verified relies on the soundness of Frama-C's static analyzer. Invoked throughout Sections 5-6.
  • domain assumption The SMT solvers used (Z3, Alt-Ergo, CVC4) are correct and the configured time/step limits suffice to find proofs when they exist.
    Verification results depend on solver behavior; timeouts could leave goals unproven yet the paper treats verified files as proven (Section 5.1).
  • domain assumption The regex patterns in Appendix A correctly distinguish ACSL annotations from other formal languages.
    Section 4.2 uses regex filters to select files; false positives would include non-ACSL files.
  • ad hoc to paper LLM-repaired files preserve the original intended behavior of the code.
    In Section 5.1, the LLM is allowed to modify code when necessary; the paper assumes this does not change the program's purpose, but no check against original behavior is described.
  • ad hoc to paper The manual inspection of every pair is accurate and complete.
    The abstract claims manual inspection confirms every pair, but the body gives no protocol, criteria, or inter-rater measures.
  • domain assumption The Stack v1 and v2 are deduplicated and representative of permissively licensed C code.
    The source data comes from The Stack; deduplication is claimed but the quality of dedup affects dataset uniqueness.
  • domain assumption CodexEmbed embeddings capture semantic similarity of code files.
    The diversity analysis (Section 7.1) uses CodexEmbed; if embeddings are not meaningful, the claimed diversity is unsupported.

how reviews work

0 comments
Cite this review

Pith. "Pith review of CASP: An evaluation dataset for formal verification of C code." pith.science (2026). https://pith.science/paper/KLVER6XT

@misc{pith2026250818798,
  author       = {Pith},
  title        = {Pith review of: CASP: An evaluation dataset for formal verification of C code},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/KLVER6XT}},
  note         = {Machine review of arXiv:2508.18798}
}
read the original abstract

Recent developments in Large Language Models (LLMs) have shown promise in automating code generation, yet the generated programs lack rigorous correctness guarantees. Formal verification can address this shortcoming, but requires expertise and is time-consuming to apply. Currently, there is no dataset of verified C code paired with formal specifications that enables systematic benchmarking in this space. To fill this gap, we present a curated evaluation dataset of C code paired with formal specifications written in ANSI/ISO C Specification Language (ACSL). We develop a multi-stage filtering process to carefully extract 506 pairs of C code and formal specifications from The Stack 1 and The Stack 2. We first identify C files annotated with formal languages. Then, we ensure that the annotated C files formally verify, and employ LLMs to improve non-verifying files. Furthermore, we post-process the remaining files into pairs of C code and ACSL specifications, where each specification-implementation pair is formally verified using Frama-C. To ensure the quality of the pairs, a manual inspection is conducted to confirm the correctness of every pair. The resulting dataset of C-ACSL specification pairs (CASP) provides a foundation for benchmarking and further research on integrating automated code generation with verified correctness.

Figures

Figures reproduced from arXiv: 2508.18798 by the authors.

Figure 1
Figure 1. ACSL specification and associated implementation in C for a function swapping two integers [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Overview of the three-step dataset construction pipeline. Step 1 involves using files from The Stack v1 and v2, which are filtered to identify C files containing ACSL specifications without external dependencies. Step 2 compiles and verifies each annotated file, and files that fail this are automatically repaired using LLMs and re-evaluated. Step 3 transforms successfully verified files into minimal specification￾im… view at source ↗
Figure 3
Figure 3. Distribution of lines of C code for each CASP pair, excluding specification and imports. Most programs are short to medium in length. The X axis indicates lines of code, and the Y axis indicates a number of occurrences. Outliers over 60 total lines of code are binned together [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Distribution of total lines of ACSL for each CASP pair. The X axis indicates the total number of lines of ACSL, and the Y axis indicates the number of occurrences. Outliers over 60 total lines of ACSL are binned together. complete, ensuring a fair comparison between da…
Figure 5
Figure 5. Figure 5: t-SNE visualization of embeddings from various datasets that verifies without any external imports (CASP source files, Frama-C problems, VecoSet, etc.). The plot shows the projection of high-dimensional embeddings into a 2D space, where proximity suggests similarity. C…
Figure 6
Figure 6. Figure 6: Nearest neighbours of various datasets (CASP source files, Frama-C problems, VecoSet, etc.). The plot shows the distance between each embedded source file, where the source file is from and how similar its nearest neighbour is. A dataset containing a wide variety of fi…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

33 extracted references · 28 canonical work pages

  1. [1]

    original-date: 2019-06-03T12:22:56Z

    ANSSI-FR/x509-parser, December 2024. original-date: 2019-06-03T12:22:56Z

    work page 2024

  2. [2]

    SyGuS-Comp 2018: Results and Analysis

    Rajeev Alur, Dana Fisman, Saswat Padhi, Rishabh Singh, and Abhishek Udupa. SyGuS-Comp 2018: Results and Analysis, April 2019. arXiv:1904.07146 [cs]

    work page Pith review arXiv 2018

  3. [3]

    Ansi/iso c specification language version 1.21, 2024

    Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. Ansi/iso c specification language version 1.21, 2024

    work page 2024

  4. [4]

    Progress on Software Verification: SV-COMP 2022

    Dirk Beyer. Progress on Software Verification: SV-COMP 2022. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 375–402, Cham,

    work page 2022

  5. [5]

    Frama-c and wp tutorial code examples

    Allan Blanchard. Frama-c and wp tutorial code examples. https://github.com/AllanBlanchard/ tutoriel_wp, 2025

    work page 2025

  6. [6]

    Formally verifying that a program does what it should: The wp plug-in

    Allan Blanchard, François Bobot, Patrick Baudin, and Loïc Correnson. Formally verifying that a program does what it should: The wp plug-in. InGuide to Software Verification with Frama-C: Core Components, Usages, and Applications, pages 187–261. Springer, 2024

    work page 2024

  7. [7]

    Language Models are Few-Shot Learners

    TomBrown,BenjaminMann,NickRyder,MelanieSubbiah,JaredDKaplan,PrafullaDhariwal,Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chris Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin ...

    work page 1901

  8. [8]

    Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian...

    arXiv 2021

Show all 33 references
  1. [9]

    Frama-c user manual for frama-c 30.0 (zinc), 2024

    Loïc Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze, Virgile Prevosto, Armand Puccetti, Julien Signoles, and Boris Yakobowski. Frama-c user manual for frama-c 30.0 (zinc), 2024

    2024

  2. [10]

    Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C. In George Eleftherakis, Mike Hinchey, and Mike Holcombe, editors,Software Engineering and Formal Methods, pages 233–247, Berlin, Heidelberg, 2012. Springer

    2012

  3. [11]

    Inductive Invariant Generation via Abductive Inference

    Isil Dillig, Thomas Dillig, Ken McMillan, and Boyang Li. Inductive Invariant Generation via Abductive Inference

  4. [12]

    Frank Dordowsky. An experimental Study using ACSL and Frama-C to formulate and verify Low- Level Requirements from a DO-178C compliant Avionics Project.Electronic Proceedings in Theoretical Computer Science, 187:28–41, August 2015. arXiv:1508.03894 [cs]

    2015 arXiv

  5. [13]

    evdenis/acsl-proved, March 2016

    Denis Efremov. evdenis/acsl-proved, March 2016. original-date: 2017-02-14T16:30:05Z

    2016

  6. [14]

    Deductive verification of unmodified linux kernel library functions

    Denis Efremov, Mikhail Mandrykin, and Alexey Khoroshilov. Deductive verification of unmodified linux kernel library functions. InLeveraging Applications of Formal Methods, Verification and Valida- tion. Verification: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, N...

    2018

  7. [15]

    ACSL by Example (Version 22.0.0) for Frama-C 22.0 (Titanium)

    Jens Gerlach. ACSL by Example (Version 22.0.0) for Frama-C 22.0 (Titanium). Fraunhofer FOKUS,

  8. [16]

    Specify what? enhancing neural specifica- tion synthesis by symbolic methods

    George Granberry, Wolfgang Ahrendt, and Moa Johansson. Specify what? enhancing neural specifica- tion synthesis by symbolic methods. In Nikolai Kosmatov and Laura Kovács, editors,Integrated Formal Methods, pages 307–325, Cham, 2025. Springer Nature Switzerland

    2025

  9. [17]

    Verifast: A powerful, sound, predictable, fast verifier for c and java

    Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. Verifast: A powerful, sound, predictable, fast verifier for c and java. InNASA formal methods sympo- sium, pages 41–55. Springer, 2011

    2011

  10. [18]

    Frama-C: A software analysis perspective.Form

    Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A software analysis perspective.Form. Asp. Comput., 27(3):573–609, May 2015

    2015

  11. [19]

    The stack: 3 tb of permissively licensed source code, 2022

    DenisKocetkov,RaymondLi,LoubnaBenAllal,JiaLi,ChenghaoMou,CarlosMuñozFerrandis,Yacine Jernite, Margaret Mitchell, Sean Hughes, Thomas Wolf, Dzmitry Bahdanau, Leandro von Werra, and Harm de Vries. The stack: 3 tb of permissively licensed source code, 2022

    2022

  12. [20]

    Mankowitz, Esme Sutherland Robson, Pushmeet Kohli, Nando de Freitas, Koray Kavukcuoglu, and Oriol Vinyals

    Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, Thomas Hubert, Peter Choy, Cyprien de Mas- son d’Autume, Igor Babuschkin, Xinyun Chen, Po-Sen Huang, Johannes Welbl, Sven Gowal, A...

    2022

  13. [21]

    Codex- embed: A generalist embedding model family for multiligual and multi-task code retrieval

    Ye Liu, Rui Meng, Shafiq Jot, Silvio Savarese, Caiming Xiong, Yingbo Zhou, and Semih Yavuz. Codex- embed: A generalist embedding model family for multiligual and multi-task code retrieval. arXiv preprint arXiv:2411.12644, 2024

    2024 arXiv

  14. [22]

    Starcoder 2 and the stack v2: The next generation, 2024

    Anton Lozhkov, Raymond Li, Loubna Ben Allal, Federico Cassano, Joel Lamy-Poirier, Nouamane Tazi, Ao Tang, Dmytro Pykhtar, Jiawei Liu, Yuxiang Wei, Tianyang Liu, Max Tian, Denis Kocetkov, Arthur Zucker, Younes Belkada, Zijian Wang, Qian Liu, Dmitry Abulkhanov, Indraneil Paul, Z...

    2024

  15. [23]

    CodeGen: An Open Large Language Model for Code with Multi-Turn Program Syn- thesis, February 2023

    Erik Nijkamp, Bo Pang, Hiroaki Hayashi, Lifu Tu, Huan Wang, Yingbo Zhou, Silvio Savarese, and Caiming Xiong. CodeGen: An Open Large Language Model for Code with Multi-Turn Program Syn- thesis, February 2023. arXiv:2203.13474 [cs]

    2023 arXiv

  16. [24]

    Towards specification-driven LLM-Based Gen- eration of embedded automotive software

    Minal Suresh Patil, Gustav Ung, and Mattias Nyberg. Towards specification-driven LLM-Based Gen- eration of embedded automotive software. In Bernhard Steffen, editor,Bridging the Gap Between AI and Reality, pages 125–144, Cham, 2025. Springer Nature Switzerland

    2025

  17. [25]

    manavpatnaik/frama-c-problems, October 2024

    Manav Patnaik. manavpatnaik/frama-c-problems, October 2024. original-date: 2020-10-27T11:44:14Z

    2024

  18. [26]

    VeCoGen: Automating Generation of Formally Verified C Code With Large Language Models

    Merlijn Sevenhuijsen, Khashayar Etemadi, and Mattias Nyberg. VeCoGen: Automating Generation of Formally Verified C Code With Large Language Models . In2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE), pages 101–112, Los Alamitos...

    2025

  19. [27]

    Post-Hoc Formal Verification of Automotive Software with Informal Requirements: An Experience Report

    Gustav Ung, Jesper Amilon, Dilian Gurov, Christian Lidström, Mattias Nyberg, and Karl Palmskog. Post-Hoc Formal Verification of Automotive Software with Informal Requirements: An Experience Report. In 2024 IEEE 32nd International Requirements Engineering Conference (RE), pages...

    2024

  20. [28]

    e x p l a n a t i o n

    Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, and Cong Tian. Enchanting program specification synthesis by large language models using static analysis and program verification. InInternational Conference on Computer Aided Verif...

    2024

  21. [31]

    Extract the full f unc ti on i m p l e m e n t a t i o n ( s i g n a t u r e and body )

  22. [32]

    Extract the ACSL s p e c i f i c a t i o n that pr ec ed es it ( t y p i c a l l y marked by /* @ or // @ )

  23. [33]

    f u n c t i o n _ i m p l e m e n t a t i o n

    I de nt if y and include only the minimal d e p e n d e n c i e s re qu ir ed for Frama - C v e r i f i c a t i o n of the fu nc ti on . This may include : - ‘# include ‘ d i r e c t i v e s ( e . g . , ‘< stdbool .h > ‘) - ‘# define ‘ macros - global c o n s t a n t s or v a ...

  24. [2020]

    CASP: An evaluation dataset for formal verification of C code 15

    Available athttps://github.com/fraunhoferfokus/acsl-by-example. CASP: An evaluation dataset for formal verification of C code 15

  25. [2022]

    Springer International Publishing

Pith tools

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