Pith. sign in

REVIEW 5 major objections 6 minor 1 cited by

Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis

T0 review · 5 major / 6 minor · reviewed 2026-08-16 · deepseek-v4-flash

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

Pith's one-line read Deepseek-R1, a reasoning LLM, can write ACSL specifications that capture a program's intended behavior rather than its buggy implementation—and adding output from symbolic tools like PathCrawler and EVA measurably steers the annotations…

desk verdict Interesting qualitative observations about steering LLM-generated formal specs, but the paper never checks whether the generated text is valid ACSL, and its two central figures appear identical. read the letter →

arxiv 2504.21061 v1 pith:RTVYGATD submitted 2025-04-29 cs.SE

George Granberry , Wolfgang Ahrendt , Moa Johansson This is my paper · ORCID
classification cs.SE
keywords specificationsynthesisACSLDeepseek-R1largelanguagemodelsneuro-symbolicmethodsFrama-CPathCrawlerEVA
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

Specification synthesis normally risks learning the bugs along with the code: a specification generated from a faulty implementation can formalize the fault instead of revealing it. This paper tries to establish that a reasoning large language model, Deepseek-R1, is largely immune to that failure: given C code and asked for ACSL contracts, the model inferred programmer intent in nearly every trial, including trials with deliberately injected bugs and anonymized function names. It also tries to show that the user can choose which contract to get—implementation or intent—by wording the prompt, and that appending output from symbolic tools (PathCrawler test cases or EVA static-analysis alarms) measurably steers the number and kind of annotations generated. If these claims hold, formal specification becomes a more practical activity: the LLM supplies flexibility and expressive postconditions, while symbolic tools supply precision and safety constraints. The paper's evidence is qualitative, based on reading the model's reasoning traces rather than on verifying the generated ACSL.

What carries the argument

The mechanism that carries the argument is an observable reasoning trace: Deepseek-R1 emits a detailed chain of thought before its answer, and the paper treats that trace as evidence of which bugs the model noticed, what intent it inferred, and whether it chose implementation or intent. Around this, the experimental apparatus consists of a 50-program C suite (intent_tests) with Basic, Famous, Mirror, and Unique categories, transformed into buggy, anonymized, and buggy-anonymized variants; and three prompt conditions on a separate 55-program PathCrawler suite: baseline, baseline plus PathCrawler input/output pairs, and baseline plus EVA alarm reports. The prompts forbid loop invariants and restrict generation to function contracts, so the comparison focuses on ACSL preconditions, postconditions, and assigns clauses.

What would settle it

Run the same prompt suite with the injected bugs concealed from the evaluators: have annotators who do not know the ground truth classify each reasoning trace for bug detection and inferred intent, and run every generated ACSL annotation through a parser and verifier against a reference intent specification; if blind bug-notice rates fall far below the reported counts, or if most annotations fail syntax or proof, the central claim is contradicted.

Watch

Extended reading notes

Core claim

The central claim, stated on the paper's own terms, is that neuro-symbolic prompting makes LLM-based specification synthesis viable for intent-sensitive contracts. Deepseek-R1 was nearly always able to identify intent: across nearly 600 generations it failed only three times, all in programs that were both buggy and anonymized, where the bug made the code resemble a different coherent program. It noticed most injected bugs (47/60 in Basic, 28/30 in Mirror, 26/30 in Unique, but only 9/30 in Famous), and in every trace where a bug was found the model explicitly consulted the prompt to decide whether to specify the implementation or the intended behavior; a simple prompt addition shifted it to intent. On the neuro-symbolic side, including symbolic analysis reduced total annotations but changed their focus: PathCrawler input/output pairs led to more abstract, case-structured postconditions, while EVA alarms were translated into preconditions that avoid runtime errors, sometimes to the point of tunnel vision that neglected the program's functional essence.

Load-bearing premise

The load-bearing premise is that reading Deepseek-R1's reasoning traces is a reliable, unbiased measure of which bugs it noticed and what intent it inferred, even though the people who injected the bugs and defined the intended behavior also judged the traces; the paper itself flags confirmation bias from prior work.

Editorial extensions

If this is right

  • Generated specifications can expose bugs instead of encoding them, provided the prompt tells the model to target intended behavior.
  • Users gain a control knob: prompt wording chooses implementation-conformant or intent-conformant contracts, and the choice of symbolic tool (PathCrawler vs EVA) shifts annotations toward postconditions or safety preconditions.
  • A raw EVA report can be dropped into a prompt with no custom translation, suggesting LLMs can absorb heterogeneous formal-tool outputs without integration code.
  • PathCrawler-style examples change the model's reasoning: it traces the examples instead of inventing its own, freeing attention for generalization—so the quality and coverage of test cases directly shapes specification quality.
  • Because EVA reports can dominate the model's attention, a workflow that wants both safety and functional content may need to combine tool outputs or explicitly rebalance the prompt.

Reading between the lines

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

  • A natural test the paper leaves open: verify the generated ACSL with Frama-C/WP; if a large share fails parsing or proof, the intent-inference claim might survive but the practical synthesis claim would need qualifiers.
  • The chain-of-thought dependence suggests the same pipeline on a non-reasoning or silent model would be far harder to steer and to evaluate; this is testable by ablating the reasoning output.
  • The EVA tunnel-vision result implies symbolic context acts as an attention magnet; combining multiple symbolic sources (e.g., EVA alarms plus PathCrawler examples) is a plausible way to get both safety preconditions and meaningful postconditions in one contract.
  • PathCrawler's minimal-path-coverage test selection is designed for testing, not specification synthesis; the paper's BugKPath failure suggests an adapted example-selection criterion—multiple varied examples per path—could materially improve synthesis, which is a concrete next experiment.
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

5 major / 6 minor

Summary. The paper investigates LLM-based synthesis of ACSL specifications for C programs using Deepseek-R1, pursuing two research directions. The first is the implementation-versus-intent problem: using a handcrafted 50-program dataset with buggy, anonymized, and combined variants, the authors qualitatively analyze Deepseek-R1's chain-of-thought to assess whether the model identifies program intent, notices injected bugs, and specifies intended rather than implemented behavior. The second direction combines the LLM with symbolic analysis by appending PathCrawler test-case outputs or EVA static-analysis reports to the prompt, and the authors report changes in annotation counts and qualitative changes in specification content. The paper concludes that Deepseek-R1 is resilient to the implementation-versus-intent problem and that neuro-symbolic prompting can steer specification synthesis toward more focused or safety-oriented annotations.

Significance. If the claims were fully supported, the paper would make a useful empirical contribution to LLM-based specification synthesis: it would demonstrate that a reasoning-focused LLM can separate intent from implementation and that symbolic tool output can influence the type and content of generated ACSL contracts. The qualitative observations about how the model uses supplied input/output examples, and the shift toward preconditions under EVA reports, are informative directions for neuro-symbolic tooling. The paper also makes the intent dataset public, which is a concrete asset for follow-up work. However, the significance is currently limited by the absence of any validation that the generated text is parseable ACSL, by a direct internal contradiction in the figures illustrating the intent-prioritization result, and by the lack of statistical support for the annotation-count claims. These issues affect the central claims, not just the presentation.

major comments (5)
  1. [§3.3, §7] The paper never verifies that the generated text blocks are syntactically valid ACSL. Section 3.3 explicitly disavows gold-standard or benchmark evaluation, and Section 7 states that verification-based evaluation was abandoned because earlier LLMs struggled with syntactic correctness, yet all annotation counts and all bug/intent qualitative claims treat the raw model output as ACSL annotations. This is load-bearing: if a substantial fraction of outputs do not parse, the counts in Fig. 8 and the bug-and-intent findings in Sections 3.4–3.7 are counting arbitrary text rather than specifications. The authors should run a Frama-C kernel parse/type pass on all outputs and report pass rates per experimental condition. The risk is concrete: the displayed annotation in Fig. 13, `ensures \result == ((a >> 1 >= -4) + ...)`, uses arithmetic over predicates and is not obviously well-formed ACSL.
  2. [§3.7, Figs. 6–7] The specification shown in Fig. 7 (captioned as generated when intent is prioritized) is byte-for-byte identical to the specification in Fig. 6 (captioned as generated when implementation is prioritized). This directly contradicts the text's claim that the revised prompt produced specifications that "more closely aligned with the intended functionality." Since the implementation-versus-intent distinction is a central contribution, the displayed evidence must be corrected to show the actual intent-prioritized output, or the claim must be revised.
  3. [§3.6, Table 1] The abstract and Section 3.6 state that the model was "almost always" able to identify bugs, but Table 1 aggregates to 110/150 overall (73%), with notably lower rates in the Famous categories (9/30 and 14/30). A 73% overall rate, and 30% on the Famous subset, does not support "almost always." The authors should report per-category rates in the text and qualify the claim accordingly, since the category dependence is itself an important finding.
  4. [§4.4, Fig. 8] The annotation-count results are presented as the quantitative support for the claim that symbolic context changes the quantity and type of generated specifications, but Fig. 8 is reported without error bars, confidence intervals, or any statistical test. With three generations per program and paired experimental conditions, the authors should report per-condition variability or perform a paired comparison before making statements such as "EVA led to an increase in preconditions" or "approximately 20% increase in annotation counts."
  5. [§6.1] The authors acknowledge that the qualitative analysis could be subject to confirmation bias. Since the bug-notice and intent-inference rates in Section 3 are derived from the authors' own reading of Deepseek-R1's reasoning traces, the paper needs a more disciplined protocol to make those rates credible: for example, independent coding by multiple annotators with inter-rater agreement, or release of the annotated traces alongside the dataset. Without this, the central qualitative claims rest on self-assessment by the same researchers who designed the bugs and defined the intended behavior.
minor comments (6)
  1. [Throughout] The tool name is inconsistently rendered as "EV A" with an extra space in many places; please use "EVA" consistently.
  2. [§4.1 vs. §6.2] Section 4.1 says the PathCrawler suite contains 55 programs, while Section 6.2 says the total dataset consisted of approximately 50 programs; please clarify the actual number used in the experiments.
  3. [Fig. 8] In the submitted text, Section 4.4 references "Fig. 8 on page 15" but the figure content itself appears to be missing or placeholder-only; please ensure the actual annotated-count figure is included.
  4. [§3.1, Table 1] Table 1 uses a category called "Unique" that is not introduced in the dataset description in Section 3.1; please define this category or remove it.
  5. [Various] There are numerous typos, including "Descrbe," "annoations," "Patchcrawler," "pr ec ond iti ons," "thostyle=csse," and "EVA T unnel-vision"; a careful proofreading pass is needed.
  6. [§4.6.3] The term "high quality examples" is defined only after the results are presented, as examples that cover all paths with multiple inputs per path; please state this criterion before the qualitative analysis so the reader can assess the claim.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper is a qualitative empirical study whose claims rest on newly collected LLM outputs, not on fitted parameters or self-citation chains that reduce to its inputs.

full rationale

This paper contains no derivation chain, fitted parameters, normalization scheme, or uniqueness theorem, so the derivation-equivalence form of circularity does not apply. The central claims—that Deepseek-R1 identifies injected bugs, infers intended behavior, and shifts its specifications when PathCrawler or EVA output is added to the prompt—are empirical observations based on newly generated traces and annotations, not consequences of the input by construction. The handcrafted intent_tests dataset is defined and judged by the authors, and Section 6.1 explicitly acknowledges the risk of confirmation bias; however, that is a validity and objectivity concern, not a circular reduction of the kind required (no equation, fitted parameter, or definitional equivalence is exhibited). The extension of and citation to the authors' prior work [12] is an acknowledged incremental research step rather than load-bearing evidence for the present results: the same authors re-ran the experiments with a different model, and the main findings here are grounded in those new runs. The absence of ACSL parsing or verification, noted in Sections 3.3 and 7, is a serious threat to the validity of the 'specification' claims, but it is a correctness risk rather than circularity. Accordingly, no circular step is identified and the score is 0.

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

The paper's claims rest on several domain assumptions about data and evaluation rather than on mathematical derivations. No free parameters are fitted. The most significant assumptions are that the Pathcrawler suite is bug-free as asserted, that the LLM's reasoning text is a trustworthy window into its computations, that the authors' handcrafted intent labels are the correct ground truth, and that unverified ACSL output can be counted and interpreted as valid specifications. These are reasonable for a qualitative study but weaken the strength of the quantitative-sounding statements.

assumptions (4)
  • domain assumption The PathCrawler test-suite programs are correct and match their intended behavior, as assured by the PathCrawler developers.
    Section 4.1 states the developers believe the 55 programs have no known bugs, and the paper uses this suite to judge whether generated annotations are accurate for 'supposedly correct programs.'
  • domain assumption Deepseek-R1's text output (reasoning chain) truthfully reflects the model's internal recognition of bugs and intent.
    Sections 3.3-3.6 use the reasoning traces as the primary evidence that bugs were noticed and that intent was inferred; this assumes the chain-of-thought is faithful and not confabulated.
  • domain assumption The author-defined intended behavior for each program in intent_tests is the correct ground truth for 'intent'.
    Section 3.1 says the dataset was handcrafted to test conflicts between implementation and intention, so the intent labels are the authors' own construction and are not independently validated.
  • domain assumption Generated ACSL annotations can be parsed and counted as requires/ensures/assigns clauses and treated as meaningful specifications without verification.
    Section 4.4 counts annotation types from the model's output, and Section 4.5 interprets them, yet the paper reports no syntax checking or proof attempts; Section 7 notes earlier LLMs had syntactic issues.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis." pith.science (2026). https://pith.science/paper/RTVYGATD

@misc{pith2026250421061,
  author       = {Pith},
  title        = {Pith review of: Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RTVYGATD}},
  note         = {Machine review of arXiv:2504.21061}
}
read the original abstract

This work is concerned with the generation of formal specifications from code, using Large Language Models (LLMs) in combination with symbolic methods. Concretely, in our study, the programming language is C, the specification language is ACSL, and the LLM is Deepseek-R1. In this context, we address two research directions, namely the specification of intent vs. implementation on the one hand, and the combination of symbolic analyses with LLMs on the other hand. For the first, we investigate how the absence or presence of bugs in the code impacts the generated specifications, as well as whether and how a user can direct the LLM to specify intent or implementation, respectively. For the second, we investigate the impact of results from symbolic analyses on the specifications generated by the LLM. The LLM prompts are augmented with outputs from two formal methods tools in the Frama-C ecosystem, Pathcrawler and EVA. We demonstrate how the addition of symbolic analysis to the workflow impacts the quality of annotations.

Figures

Figures reproduced from arXiv: 2504.21061 by the authors.

Figure 1
Figure 1. Example PathCrawler input/outputs for BubbleSort [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Example EVA report manifest in practice. By examining how the model responds to mismatches between implementation and intent, we aim to understand whether and how LLMs can identify discrepancies, infer programmer intent, and produce specifications that go beyond simply restating buggy behavior. Specifically, we aim to answer the following questions: (1) How capable are LLMs at identifying the intent of a program? (2… view at source ↗
Figure 3
Figure 3. Prompt used for generating ACSL annotations [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (18 more)
Figure 4
Figure 4. Figure 4: Prompt used for generating ACSL annotations with PathCrawler as additional context [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: Prompt used for generating ACSL annotations with EVA as additional context [PITH_FULL_IMAGE:figures/full_fig_p008_5.png]
Figure 6
Figure 6. Figure 6: Specification generated for buggyu palindome.c when implementation is prioritized [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]
Figure 7
Figure 7. Figure 7: Specification generated for buggyu palindome.c when intent is prioritized [PITH_FULL_IMAGE:figures/full_fig_p013_7.png]
Figure 8
Figure 8. Figure 8: Annotation-type counts for each prompt 4.5 Annotation Counts 4.5.1 More is Not Better. An important point to consider when interpreting the annotation counts presented in [PITH_FULL_IMAGE:figures/full_fig_p015_8.png]
Figure 9
Figure 9. Figure 9: Snippet of reasoning done for ADPCM.c (Adaptive differential pulse-code modulation) when provided with pathcrawler output [PITH_FULL_IMAGE:figures/full_fig_p016_9.png]
Figure 10
Figure 10. Figure 10: Snippet of reasoning done for ADPCM.c (Adaptive differential pulse-code modulation) when no input/output examples are [PITH_FULL_IMAGE:figures/full_fig_p017_10.png]
Figure 11
Figure 11. Figure 11: Specification generated for TestShiftRT For example, in the PathCrawler output and accompanying reasoning showed in [PITH_FULL_IMAGE:figures/full_fig_p018_11.png]
Figure 12
Figure 12. Figure 12: Interesting snippets from the reasoning process being the specification generated for TestShiftRT with PathCrawler output in the [PITH_FULL_IMAGE:figures/full_fig_p019_12.png]
Figure 13
Figure 13. Figure 13: Specification generated for TestShiftRT with no PathCrawler output in the prompt [PITH_FULL_IMAGE:figures/full_fig_p020_13.png]
Figure 14
Figure 14. Figure 14: PathCrawler output for Bsearch.c input_len,input_buffer[0],input_buffer[1],input_buffer[2],input_buffer[3],input_msg[0],input_msg[1],output,verdict 2,0,0,0,0,0,0,0,0,unknown 3,0,0,0,0,10,46,0,0,46,46,unknown 2,0,0,0,0,10,46,10,46,46,unknown 2,0,0,0,0,10,0,10,0,unknown…
Figure 15
Figure 15. Figure 15: PathCrawler output and reasoning for BugKPath.c [PITH_FULL_IMAGE:figures/full_fig_p020_15.png]
Figure 16
Figure 16. Figure 16: PathCrawler output and reasoning for BugKPath.c [PITH_FULL_IMAGE:figures/full_fig_p021_16.png]
Figure 17
Figure 17. Figure 17: PathCrawler output and reasoning for BugKPath.c [PITH_FULL_IMAGE:figures/full_fig_p022_17.png]
Figure 18
Figure 18. Figure 18: Alias5 specification generated with an EVA report as context [PITH_FULL_IMAGE:figures/full_fig_p023_18.png]
Figure 19
Figure 19. Figure 19: Tritype specification generated with an EVA report as context [PITH_FULL_IMAGE:figures/full_fig_p024_19.png]
Figure 20
Figure 20. Figure 20: Tritype specification generated with the baseline prompt [PITH_FULL_IMAGE:figures/full_fig_p025_20.png]
Figure 21
Figure 21. Figure 21: Reasoning performed about an EVA report run on Tritype.c [PITH_FULL_IMAGE:figures/full_fig_p025_21.png]

Discussion (0). Continue with ORCID 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. Vibe Coding vs. Agentic Coding: Fundamentals and Practical Implications of Agentic AI

    cs.SE 2025-05 conditional novelty 3.0 of 10

    A qualitative taxonomy positions vibe coding and agentic coding as complementary paradigms rather than rivals in AI-assisted software development.

Reference graph

Works this paper leans on

36 extracted references · 21 canonical work pages · cited by 1 Pith paper

  1. [1]

    In: International Sympo- sium on Leveraging Applications of Formal Methods

    Ahrendt, W., Gurov, D., Johansson, M., Rümmer, P.: TriCo—triple co-piloting of implementation, specification and tests. In: International Sympo- sium on Leveraging Applications of Formal Methods. pp. 174–187. Springer (2022)

    work page 2022

  2. [2]

    Alhessi, Y ., Einarsdóttir, S.H., Granberry, G., First, E., Johansson, M., Lerner, S., Smallbone, N.: Lemmanaid: Neuro-symbolic lemma conjecturing (2025), https://arxiv.org/abs/2504.04942

    arXiv 2025

  3. [3]

    CEA-LIST, Saclay, France, Tech

    Baudin, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y ., Prevosto, V .: ACSL: ANSI C specification language. CEA-LIST, Saclay, France, Tech. Rep. v1 2 (2008)

    work page 2008

  4. [4]

    In: Benzmüller, C., Miller, B

    Blaauwbroek, L., Urban, J., Geuvers, H.: The tactician – a seamless, interactive tactic learner and prover for coq. In: Benzmüller, C., Miller, B. (eds.) Intelligent Computer Mathematics. pp. 271–277. Springer International Publishing, Cham (2020)

    work page 2020

  5. [5]

    In: Proceedings of the 27th ACM SIGSOFT international symposium on software testing and analysis

    Blasi, A., Goffi, A., Kuznetsov, K., Gorla, A., Ernst, M.D., Pezzè, M., Castellanos, S.D.: Translating code comments to procedure specifications. In: Proceedings of the 27th ACM SIGSOFT international symposium on software testing and analysis. pp. 242–253 (2018)

    work page 2018

  6. [6]

    In: 18th International Conference on Verification Model Checking and Abstract Interpretation (VMCAI 2017)

    Blazy, S., Bühler, D., Yakobowski, B.: Structuring abstract interpreters through state and value abstractions. In: 18th International Conference on Verification Model Checking and Abstract Interpretation (VMCAI 2017). Proceedings of the International Conference on Verification Model Checking and Abstract Interpretation, vol. 10145 LNCS, pp. 112–130. Paris...

    doi:10.1007/978-3-319-52234-0_7 2017

  7. [7]

    Advances in neural information processing systems 33, 1877–1901 (2020)

    Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J.D., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., et al.: Language models are few-shot learners. Advances in neural information processing systems 33, 1877–1901 (2020)

    2020

  8. [8]

    In: Formal Methods for Industrial Critical Systems: 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013

    Davis, J.A., Clark, M., Cofer, D., Fifarek, A., Hinchman, J., Hoffman, J., Hulbert, B., Miller, S.P., Wagner, L.: Study on the barriers to the indus- trial adoption of formal methods. In: Formal Methods for Industrial Critical Systems: 18th International Workshop, FMICS 2013, Madrid, Spain, September 23-24, 2013. Proceedings 18. pp. 63–77. Springer (2013)

    work page 2013

Show all 36 references
  1. [9]

    Science of computer programming 69(1-3), 35–45 (2007) Manuscript submitted to ACM Seeking Specifications 29

    Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The daikon system for dynamic detection of likely invariants. Science of computer programming 69(1-3), 35–45 (2007) Manuscript submitted to ACM Seeking Specifications 29

    2007

  2. [10]

    In: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering

    First, E., Rabe, M.N., Ringer, T., Brun, Y .: Baldur: Whole-proof generation and repair with large language models. In: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. p. 1229–1241. ESEC/FSE 2...

    2023

  3. [11]

    Information Processing Letters 77(2-4), 97–108 (2001)

    Flanagan, C., Joshi, R., Leino, K.R.M.: Annotation inference for modular checkers. Information Processing Letters 77(2-4), 97–108 (2001)

    2001

  4. [12]

    In: International Confer- ence on Integrated Formal Methods

    Granberry, G., Ahrendt, W., Johansson, M.: Specify what? Enhancing neural specification synthesis by symbolic methods. In: International Confer- ence on Integrated Formal Methods. pp. 307–325. Springer (2024)

    2024

  5. [13]

    Greiner, S., Bühlmann, N., Ohrndorf, M., Tsigkanos, C., Nierstrasz, O., Kehrer, T.: Automated generation of code contracts: Generative ai to the rescue? In: Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences. pp. 1–...

    2024

  6. [14]

    (eds.) Fundamental Approaches to Software Engineering

    Janßen, C., Richter, C., Wehrheim, H.: Can ChatGPT support software verification? In: Beyer, D., Cavalcanti, A. (eds.) Fundamental Approaches to Software Engineering. pp. 266–279. Springer Nature Switzerland, Cham (2024)

    2024

  7. [15]

    In: Oh, A.H., Agarwal, A., Belgrave, D., Cho, K

    Jiang, A.Q., Li, W., Tworkowski, S., Czechowski, K., Odrzygó´ zd´ z, T., Miło´s, P., Wu, Y ., Jamnik, M.: Thor: Wielding hammers to integrate language models and automated theorem provers. In: Oh, A.H., Agarwal, A., Belgrave, D., Cho, K. (eds.) Advances in Neural Information P...

    2022

  8. [16]

    In: NeSy 2023, 17th International Workshop on Neural-Symbolic Learning and Reasoning (2023)

    Johansson, M., Smallbone, N.: Exploring mathematical conjecturing with large language models. In: NeSy 2023, 17th International Workshop on Neural-Symbolic Learning and Reasoning (2023)

    2023

  9. [17]

    arXiv preprint arXiv:2311.07948 (2023)

    Kamath, A., Senthilnathan, A., Chakraborty, S., Deligiannis, P., Lahiri, S.K., Lal, A., Rastogi, A., Roy, S., Sharma, R.: Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948 (2023)

    2023 arXiv

  10. [18]

    Formal Aspects of Computing 27(3), 573–609 (2015)

    Kirchner, F., Kosmatov, N., Prevosto, V ., Signoles, J., Yakobowski, B.: Frama-c: A software analysis perspective. Formal Aspects of Computing 27(3), 573–609 (2015). https://doi.org/10.1007/s00165-014-0326-7

    2015 doi

  11. [19]

    Springer Cham (2024)

    Kosmatov, N., Prevosto, V ., Signoles, J.: Guide to Software Verification with Frama-C. Springer Cham (2024). https://doi.org/10.1007/978-3-031- 55608-1

    2024 doi

  12. [20]

    Journal of Systems and Software p

    Lathouwers, S., Huisman, M.: Survey of annotation generators for deductive verifiers. Journal of Systems and Software p. 111972 (2024)

    2024

  13. [21]

    arXiv preprint arXiv:2401.08807 (2024)

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

    2024 arXiv

  14. [22]

    Mugnier, E., Gonzalez, E.A., Jhala, R., Polikarpova, N., Zhou, Y .: Laurel: Generating Dafny assertions using large language models (May 2024), arXiv 2405.16792

    2024 arXiv

  15. [23]

    In: Proceedings of ICLR (2021)

    Rabe, M.N., Lee, D., Bansal, K., Szegedy, C.: Mathematical reasoning via self-supervised skip-tree training. In: Proceedings of ICLR (2021)

    2021

  16. [24]

    SIGSOFT Softw

    Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. SIGSOFT Softw. Eng. Notes 30(5), 263–272 (sep 2005). https://doi.org/10.1145/1095430.1081750, https://doi.org/10.1145/1095430.1081750

    2005

  17. [25]

    Signoles, J.: E-ACSL: Executable ANSI/ISO C Specification Language (2011), http://frama-c.com/download/e-acsl/e-acsl.pdf

    2011

  18. [26]

    In: Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)

    Silva, A.F., Mendes, A., Ferreira, J.a.F.: Leveraging large language models to boost Dafny’s developers productivity. In: Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE). p. 138–142. FormaliSE ’24, Associatio...

    2024

  19. [27]

    arXiv preprint arXiv: Arxiv-2404.12534 (2024)

    Song, P., Yang, K., Anandkumar, A.: Towards large language models as copilots for theorem proving in Lean. arXiv preprint arXiv: Arxiv-2404.12534 (2024)

    2024 arXiv

  20. [28]

    In: Cerone, A

    Tyler, B.: Formal methods adoption in industry: An experience report. In: Cerone, A. (ed.) Formal Methods for an Informal World: ICTAC 2021 Summer School, Virtual Event, Astana, Kazakhstan, September 1–7, 2021, Tutorial Lectures. pp. 152–161. Springer International Publishing,...

    2023 doi

  21. [29]

    In: Proceedings of CICM (2020)

    Urban, J., Jakub˚ uv, J.: First neural conjecturing datasets and experiments. In: Proceedings of CICM (2020). https://doi.org/10.1007/978-3-030-53518- 6_24

    2020 doi

  22. [30]

    arXiv preprint arXiv:2305.11792 (2023)

    Wang, H., Wang, R., Mi, F., Wang, Z., Xu, R., Wong, K.F.: Chain-of-thought prompting for responding to in-depth dialogue questions with llm. arXiv preprint arXiv:2305.11792 (2023)

    2023 arXiv

  23. [31]

    arXiv preprint arXiv:2310.18457 (2023)

    Welleck, S., Saha, R.: LLMSTEP: LLM proofstep suggestions in lean. arXiv preprint arXiv:2310.18457 (2023)

    2023 arXiv

  24. [32]

    In: International Conference on Computer Aided Verification

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

    2024

  25. [33]

    arXiv preprint arXiv:2302.11382 (2023)

    White, J., Fu, Q., Hays, S., Sandborn, M., Olea, C., Gilbert, H., Elnashar, A., Spencer-Smith, J., Schmidt, D.C.: A prompt pattern catalog to enhance prompt engineering with ChatGPT. arXiv preprint arXiv:2302.11382 (2023)

    2023 arXiv

  26. [34]

    In: European Dependable Computing Conference

    Williams, N., Marre, B., Mouy, P., Roger, M.: Pathcrawler: Automatic generation of path tests by combining static and dynamic analysis. In: European Dependable Computing Conference. pp. 281–292. Springer (2005)

    2005

  27. [35]

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

    Wu, G., Cao, W., Yao, Y ., Wei, H., Chen, T., Ma, X.: Llm meets bounded model checking: Neuro-symbolic loop invariant inference. In: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. pp. 406–417 (2024)

    2024

  28. [36]

    In: Neural Information Processing Systems (NeurIPS) (2023) Manuscript submitted to ACM

    Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., Anandkumar, A.: LeanDojo: Theorem proving with retrieval- augmented language models. In: Neural Information Processing Systems (NeurIPS) (2023) Manuscript submitted to ACM

    2023

Pith tools

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