Conceptio › Archive › arXiv CS
arXiv CS open access

Decalage: Uncovering the Gap Between Model-Generated Reasoning and Actual Code Implementation in Small Language Models

Saif Uddin Mahmud et al. · arxiv_cs
arXiv CS · Papers
Open Source ↗Direct PDF ↓
software-architecturesoftware-engineeringtesting
Agentic code generation often asks a model to explain its reasoning before it writes code, and a common way to make such a workflow safer is to add a security instruction to the prompt. We test what that instruction does in small language models, which are attractive because they run locally and che
Conceptio Open Archive

Analyze & explore related research in Conceptio

Connect this record directly into your research workflow or AI agent. Explore citations across open repositories, query full text, and export structured proof bundles.

Décalage: Uncovering the Gap Between Security-Oriented Reasoning and Actual Code Implementation in Small Language Models Afsana Tasnim

Saif Uddin Mahmud

arXiv:2611.11721v1 [cs.SE] 9 Nov 2026

University of Texas at Arlington Arlington, TX, USA sxm8931@mavs.uta.edu

Ahmed Ryan

University of Texas at Arlington University of Alabama Tuscaloosa, AL, USA Arlington, TX, USA aryan@crimson.ua.edu axt0868@mavs.uta.edu

Abstract—Agentic code generation often asks a model to explain its reasoning before it writes code, and a common way to make such a workflow safer is to add a security instruction to the prompt. We test what that instruction does in small language models, which are attractive because they run locally and cheaply. Four open code models of 1.5B to 3B parameters generate C++ from 166 sections of eleven public requirements documents, once with a general prompt and once with a secure prompt. The secure prompt more than doubles the share of reasoning about validation, resource handling and threats, and we find no evidence that the rise is larger for requirements with security content. The code changes only in part. Among functions with a body and reasoning, the share with a check that our lexical test recognises rises from 23% to 39%, but more than a quarter of the functions remain stubs, compile rates stay low, and half or more of the functions whose reasoning mentions a check contain no such check. Two rounds of compiler-feedback repair leave more than 80% of sections unusable, and neither cppcheck nor an exploratory ESBMC run separates the prompts on the usable code. A hand check by two annotators supports the stub measure and the direction of the reasoning result. For small models, a security instruction changes the reasoning broadly but the code only in part, so the reasoning should be checked against the code rather than trusted. Index Terms—LLM agents, code generation, secure coding, reasoning traces, faithfulness, small language models

Md Rayhanur Rahman University of Alabama Tuscaloosa, AL, USA mrahman87@ua.edu

Less is known about what such an instruction does to the reasoning the model writes, and whether the code changes with it. Work on chain-of-thought faithfulness shows that stated reasoning can leave out the factors that drive a model’s answer [3], [4], but it concentrates on question answering rather than code. We study this for small models generating C++ from software requirements specifications (SRS). A two-stage workflow plans the functions for each requirement section and then implements each one with 3 to 6 reasoning steps. Every section is run under a general and a secure prompt, with nothing else changed. We ask five questions.

I. I NTRODUCTION

RQ1 How does a secure prompt change the content of the reasoning, and does the change differ across models? RQ2 Does the change follow the requirement, or only the prompt? RQ3 How complete is the generated code (stubs, compile rate), and does the secure prompt change that? RQ4 When the reasoning says a check will be added, does the code contain one? RQ5 When compiler errors are fed back in repair rounds, does the code become usable, and does the secure prompt change that?

Agentic code generation splits a task into steps. A planner decides which functions a requirement needs, an implementer writes each one, and a compiler or static analyser can feed results back for repair. At each step the model is often asked to explain its reasoning before the code. A developer reads that reasoning first, and it shapes how far they trust the code. Small language models (here, models with at most 3B parameters) are attractive for such workflows because they comfortably run on a laptop GPU, keep code and requirements on premises, and cost little per call. They are also weaker than the models most code generation studies evaluate, and their limits in agentic settings are less well documented. A common way to make a workflow safer is to add a security instruction to the system prompt. Prior work shows that code models produce vulnerable code at a substantial rate [1] and that prompting or tuning can shift this rate [2].

The workflow goes straight from the requirement text to code. It skips the steps that usually sit between them in software development: domain modelling and class and sequence diagrams. We made this choice on purpose. It tests what a small model does with the requirement alone, and it matches how these models are often used. It also differs from real development, where a design comes before the code. RQ1 and RQ2 concern the reasoning, RQ3 the code, RQ4 the link between them, and RQ5 the agentic repair loop. The answers point the same way. The secure prompt more than doubles the share of reasoning about validation, resource handling and threats, and the rise is not detectably larger for requirements with security content. The code follows only in part. Among functions with a body and reasoning, the share with a lexically recognised check rises from 23% to 39%. But more than a quarter of the generated functions are stubs

under either prompt, compile and usability rates show no clear difference between prompts, and half or more of the functions whose reasoning mentions a check contain no recognised check. Two repair rounds with compiler feedback fill many stubs and roughly double the share of usable sections, yet most sections remain unusable. Static analysis and an exploratory bounded model check of the usable code do not show a clear security difference between the prompts, but the checked sets are small and differ between prompts. A hand check of the measures by two annotators supports the stub measure. It led us to revise three keyword lists that matched generic words. The revised core measure is precise but misses more than half of what the annotators mark. Both annotators see the same direction of change, and on their small sample a larger one. Our contributions are: • a paired comparison of the reasoning and code of four small code models under a general and a secure prompt, on the same requirement sections; • evidence that the secure prompt changes the reasoning broadly but the code only in part: stubs, compile rates and usability show no clear difference, and the reasoning often mentions checks that a lexical test does not find in the code; • an evaluation of compiler-feedback repair and static analysis, and an exploratory bounded model check of the generated code, including where ESBMC fails on generated C++;

Reasoning and faithfulness. Chain-of-thought prompting elicits intermediate steps [11]. Turpin et al. showed that explanations can systematically misrepresent the cause of a prediction [3], and Lanham et al. measured how much answers depend on the stated chain [4]. Wiegreffe et al. define association between a label and its free-text rationale as a necessary property of faithful rationales and test it for joint predict-andrationalize models [12]. Our follow-through measure asks a narrower, code-specific question: does the function contain a lexically recognised check when its reasoning mentions one? Small models and agentic workflows. ReAct interleaves reasoning with tool calls [13], and repair workflows for code add compiler and analyser feedback. SWE-bench evaluates models on resolving real GitHub issues [14], and SelfDebugging has a model use execution results and its own explanation of its code to repair it [15]. Both were evaluated with much larger models than ours. Wei generates code from requirements documents in steps: the model extracts functional requirements, builds object-oriented models, and only then writes tests and code [16]. Our small models get no such steps. They write code directly from the requirement text. Belcak et al. argue that small language models are sufficient for many agentic subtasks and cheaper to run [17]. Our results add evidence on where that holds and where it does not for requirements-to-code generation. Our pipeline has a plan stage, a per-function stage, and a repair loop that feeds compiler errors back to the model (RQ5).

II. R ELATED W ORK

III. M ETHOD

Security of generated code. Pearce et al. found that about 40% of Copilot completions in security-relevant scenarios were vulnerable [1]. A user study found that participants with an AI assistant wrote less secure code and were more confident in it [5], while a study of 58 students writing C found the assistant raised the rate of critical bugs by no more than 10% [6]. Khoury et al. found that ChatGPT-generated C and C++ was often insecure on the first attempt, with follow-up prompts helping only marginally [7]. LLMSecEval supplies natural-language prompts for evaluating the security of generated code [8]. CyberSecEval benchmarks insecure code suggestions and compliance with attack requests across seven models [9]. SVEN steers a model toward or away from vulnerable output with learned prefixes [2]. Mahmud et al. checked 8,918 C++ programs written by three large openweight models and by humans with functional testing, static analysis, sanitizers and bounded model checking [10]. The AIwritten code was about twice as likely to trigger a confirmed runtime violation, while static analysis alone made the two look equally safe. Their programs solve competitive programming problems from CodeContests: short, self-contained tasks with fixed input and output, which do not reflect how software is built from requirements. They also do not examine the reasoning the models write. These studies measure the code. We start from requirements in public SRS documents, and we measure what the model says about security when asked to be secure, and whether its code backs that up.

A. Workflow Fig. 1 shows the workflow. For each requirement section it makes one plan call and one function call per planned function. The plan call returns a JSON list of functions (name, signature, one-line purpose) and the shared type declarations the functions use, with at most five functions. If the text describes nothing that can be implemented, the list is empty. Each function call receives the requirement text, the shared declarations, the plan, and the functions already written, and returns JSON with a reasoning field of 3 to 6 short steps “explaining how and why you implement it this way” and a code field with one function definition. Each step therefore belongs to one function. The assembled file is compiled with g++ -std=c++17 -fsyntax-only. The two prompts differ only in the opening of the system prompt. The general prompt says “Write C++ code.” The secure prompt says “Write secure, robust, and defensive C++ code. Follow best practices for input validation, memory safety, and safe resource handling.” Both then share the same rules (no main, no #include, no mutable globals, reply only with JSON). B. Data and models Requirements come from PURE, a dataset of 79 public requirements documents collected from the Web [18]. PURE labels each document by source: a university case study or assignment (U), or a company or public body (I). Its authors

System prompt, one of two: general: “Write C++ code.” secure: “Write secure, robust, and defensive C++ code . . . ”

SRS section

Plan call

Function call

functions, signatures, shared types

one per planned function

Reasoning

RQ4

Assemble and compile g++ -fsyntax-only

Code

3–6 steps

one definition

RQ1, RQ2

RQ3

repair rounds (RQ5): compiler errors fed back

Fig. 1. The two-stage workflow. Both calls see the same system prompt. Each function call returns the reasoning and the code that RQ1–RQ4 analyse. The dashed loop is the compile-repair round of RQ5.

TABLE I T HE 11 PURE DOCUMENTS . S OURCE : I = COMPANY OR PUBLIC BODY, U = UNIVERSITY. S ECTIONS ARE THE UNITS OF REQUIREMENT TEXT GIVEN TO THE MODELS . F UNCTIONS IS THE MEAN NUMBER OF FUNCTIONS THE MODELS WROTE PER RUN , OVER THE FOUR MODELS AND TWO PROMPTS .

Document

Source

Sections

Functions

microcare (vouchers) keepass (passwords) themas (energy) blitdraft (laboratory) cctns (police) dii (defence XML)

I I I I I I

28 27 22 12 9 6

122 94 72 42 38 24

gamma j (web store) video search (video) peering (CDN) get real 0.2 (outreach) qheadache (game)

U U U U U

24 14 12 10 2

95 60 50 38 7

166

643

Total

converted 18 of the documents to a uniform XML format, and we draw from these. All our models run locally on a single laptop with an 8 GB GPU, which could not cover 18 documents with four models, two prompts and repair rounds, so we use eleven documents, balanced between the two sources. We use every requirement section of each, 166 sections in all, identical across prompts and models (Table I). Six documents are of source I and contribute 104 sections: a police casemanagement system of the Government of India, a US defence XML services specification, an energy management system, a voucher management system, the KeePass password manager and a laboratory information system. Five are of source U and contribute 62 sections: a content delivery network peering system, a web store, a university outreach website, a video search engine and a small game.

We use four instruction-capable code models served through Ollama: Qwen2.5-Coder 1.5B and 3B [19], OpenCoder 1.5B [20], and DeepCoder 1.5B, a code model tuned for reasoning. We chose code-specialized models on purpose, because they are the small models built to support software engineering tasks and the ones a developer would run locally for this one. Decoding is greedy (temperature 0, seed 0) for all models. DeepCoder writes a long native thinking trace before its answer, so it gets an 8,192-token output budget and a 12,288-token context; the others get 1,536 and 4,096. Each model and prompt is run once. The unit of analysis is a (model, requirement) pair with at least one reasoning step under both prompts. Each run plans its own functions, so counts are not comparable across prompts. We compare rates per step or per function inside the pair. This yields 640 pairs: 166 for each of Qwen 1.5B, Qwen 3B and OpenCoder, and 142 for DeepCoder. DeepCoder returned malformed output for at least one function in more than half of the sections, and 24 sections have no reasoning from it under at least one prompt. The four models wrote 5,145 functions, about 640 per model and prompt, with 16,872 reasoning steps. C. Measures Content categories (RQ1, RQ2). Each step is tagged by phrase patterns in six categories: validation, memory and resources, error handling, threat and safety words, secrets and access, and prevention (avoid, prevent, guard, protect). “Core” is the union of validation, memory and resources, threat, and prevention; error handling and secrets are excluded from it because requirements often call for them directly. Echo marks steps that repeat wording from the secure prompt (input validation, memory safety, best practices, defensive, and similar). Core without echo recomputes the core tag after deleting echo phrases. We revised the keyword lists once, after the hand check in Section VI. We removed generic words that the annotators did not accept (ensure, robust, secure, safe,

and bare pointer, resources and null as memory words), and counted null as validation. The results use the revised lists. We also report the original lists as a sensitivity row. The prompt asks for 3 to 6 steps per function. Under greedy decoding DeepCoder sometimes loops and writes far more (up to 424 steps for one function; 26 of its 448 general-prompt functions with reasoning hold 44% of its general-prompt steps), which would let a few runaway outputs dominate its rates. We therefore analyse the first six steps of every function, 15,924 steps in all. Without this cap the pooled results are within about one point of those we report, but DeepCoder’s per-model interval becomes wide enough to include zero. Form (RQ1). Words per step, steps per function, and the share of steps with a hedge (might, probably), an obligation (should, must), a conditional (if, unless), first-person wording, or a concrete code reference (backticked text, a call such as f(), snake case or camelCase identifiers). Requirement relevance (RQ2). A pair is “securityrelevant” when the requirement text matches at least two distinct terms from a list (password, authenticate, encrypt, permission, privilege, credential, user input, validate, privacy, audit, session, network, database, key, token, file, and similar). This gives 100 relevant and 540 other pairs. Implementation (RQ3). Each function body is assigned to one of five classes by a heuristic over its statements, with comments removed: empty (no body or no statement), output or trivial only (printing, constant returns, bare declarations), placeholder (wording such as “in a real implementation”, “simulate” or “TODO”), minimal (a few statements and no control flow), and logic (control flow or at least three nontrivial statements). We call the first three classes stubs. We also report whether the assembled file compiles and whether it is usable: it compiles and no planned function is a stub. Usable does not mean functionally correct: we run no tests. Follow-through (RQ4). We consider every function whose body has at least one statement other than a placeholder comment and that has at least one reasoning step: 1,982 functions under the general prompt and 2,020 under the secure prompt. This excludes fewer functions than the RQ3 stub classes. The mention flag is set if any step names a check (validate, check that/if/whether, verify, ensure, null, empty, bounds, invalid, throw, exception). The code flag is set if the function body, with comments removed, contains a null or emptiness test, a size comparison, a throw or catch, an .at() or find() call, or an if on a comparison that returns or throws. We report the code-flag rate among functions that do and do not mention a check. The flags are coarse: they show whether the function has a recognised check, not whether it is the check the reasoning names. D. Repair rounds (RQ5) A compile-repair round takes every section of the previous round that is not usable and asks the model, with the same system prompt, to repair it one function at a time. A function whose code has compiler errors gets the errors (with line numbers relative to the function) and its own code, and may

also return type declarations to add. A function that is missing or has no body gets the original implement prompt again. A section whose plan failed is planned again. Usable sections are carried forward unchanged. Round C1 starts from the first generation (R0) and round C2 from C1. Repair calls use temperature 0.2 (0.6 for DeepCoder, which loops at low temperature) with a seed derived from the section, prompt, round and function. If a repair call returns no body, the function is left out of the output, so we count missing planned functions as stubs when comparing rounds. We report both rounds pooled for Qwen 1.5B, Qwen 3B and OpenCoder. DeepCoder needs about four hours per prompt for one round on our GPU, so we report it separately. We do not analyse the reasoning written during repair. E. Statistics For each rate we report the pooled secure-minus-general difference with a 95% percentile bootstrap interval over requirement sections (2,000 resamples), keeping each section’s pairs together. We also report a Wilcoxon signed-rank test on the pair-level differences. We read intervals first and treat the p values with care, since many tags are tested together. IV. R ESULTS A. RQ1: what does the reasoning talk about? Table II and Fig. 2 give the shifts. Under the general prompt, 7.1% of steps fall in a core security category. Under the secure prompt 18.1% do, a rise of 11.0 points (CI 9.5 to 12.4, p < 10−31 ), about two and a half times the share. Validation, memory and resources, threat, and prevention all rise with intervals that exclude zero. Error handling rises by 4.6 points. Secrets and access is the exception: +0.4 points, CI [−0.4, 1.2]. Echo accounts for a small part. Steps that repeat the prompt’s phrases go from 0.08% to 4.1% of steps. Deleting those phrases leaves the core shift at +9.1 points (CI 7.8 to 10.5), so the instruction changes what the models write about beyond copying it back. The original keyword lists give a larger share and a similar shift: 15.7% to 27.3% with echo removed, +11.7 points (CI 10.0 to 13.3). The result holds under both lists. It also holds without the memory and threat tags, which the hand check could not validate: validation and prevention alone rise from 5.9% to 13.5% (+7.6 points, CI 6.4 to 8.8). The hand check in Section VI found that the original memory, threat and prevention lists matched mostly generic words, which is why we revised them. The form of the steps changes less. Length shows no clear change: 24.4 words per step under the general prompt and 23.8 under the secure one (CI for the difference −1.5 to +0.2), and the number of steps per function is similar (3.12 and 3.10). Obligation and first-person wording barely change. The secure prompt makes the reasoning more conditional and less concrete. Steps with a conditional rise from 22.8% to 27.9% (CI +3.3 to +7.0 points, p < 10−4 ). Steps with a concrete code reference fall from 46.5% to 38.2% (CI −10.5 to −6.0 points, p < 10−5 ). Hedges rise slightly,

TABLE II S HARE OF STEPS WITH EACH CONTENT TAG , GENERAL VS SECURE PROMPT, 640 PAIRED ( MODEL , REQUIREMENT ) CASES . D IFFERENCES IN PERCENTAGE POINTS WITH 95% BOOTSTRAP CI OVER REQUIREMENTS . TAGS USE THE REVISED KEYWORD LISTS . T HE VALIDATION + PREVENTION ROW HAS ECHO REMOVED .

Tag

General Secure

Diff. [95% CI] +8.0 [6.8, 9.2] +2.7 [2.0, 3.3] +4.6 [3.5, 5.8] +0.9 [0.6, 1.3] +0.4 [−0.4, 1.2] +1.8 [1.2, 2.3]

Validation Memory / resources Error handling Threat / safety words Secrets / access Prevention

5.1 0.5 4.2 0.8 4.8 0.9

13.1 3.2 8.8 1.8 5.2 2.7

Core (union of four) Core, echo removed Core, no echo, old lists Validation + prevention Echo

7.1 7.1 15.7 5.9 0.08

18.1 +11.0 [9.5, 12.4] 16.2 +9.1 [7.8, 10.5] 27.3 +11.7 [10.0, 13.3] 13.5 +7.6 [6.4, 8.8] 4.1 +4.0 [3.3, 4.7]

Change in share of reasoning steps, paired by requirement validation

+8.0

memory / resources threat and safety words

+2.7 +0.9

prevention (avoid, prevent, guard)

+1.8

error handling secrets and access repeats the prompt's wording any core category, wording removed

qwen25coder3b

By model

deepcoder15b opencoder15b qwen25coder15b

general prompt secure prompt

6 8 10 12 14 16 18 % of steps in a core security category (prompt wording removed)

Fig. 3. Share of steps in a core security category (prompt wording removed) per model, general vs secure prompt. TABLE III S ECURE - MINUS - GENERAL SHIFT ( POINTS ) BY REQUIREMENT RELEVANCE . I NTERACTION IS RELEVANT MINUS OTHER .

Tag Core Validation Memory / resources Threat / safety Prevention Secrets / access

Rel. (100) Other (540) Interaction [95% CI] +9.8 +7.0 +2.1 +1.5 +1.9 +3.2

+11.2 +8.2 +2.8 +0.9 +1.8 −0.1

−1.4 [−5.2, 2.4] −1.2 [−4.2, 2.2] −0.7 [−2.1, 0.6] +0.6 [−0.3, 1.6] +0.1 [−1.4, 1.8] +3.3 [0.2, 6.6]

+4.6 +0.4 +4.0 +9.1

0 2 4 6 8 10 points more steps with this content (secure minus general)

Fig. 2. Change in the share of steps per content category, secure minus general. Bars are 95% bootstrap intervals over requirement sections.

from 0.9% to 1.3%. With seven form measures examined, the conditional and concrete-reference differences survive a Bonferroni correction and the hedge difference does not. The drop in concrete references is largest for Qwen 3B (−17.0 points, CI −20.8 to −13.0) and also clear for DeepCoder (−7.5, CI −12.2 to −2.7). All four models move in the same direction, by different amounts (Fig. 3). With echo removed, the core share rises from 7.7% to 18.3% for DeepCoder, 6.7% to 16.3% for OpenCoder, 9.3% to 12.1% for Qwen 1.5B, and 5.3% to 18.4% for Qwen 3B. Qwen 1.5B has the smallest shift (+2.8, CI 0.4 to 5.3) and Qwen 3B the largest (+13.1, CI 11.0 to 15.2). Qwen 3B also copies the prompt most: 7.7% of its secure-prompt steps are echo, against 1.5% to 2.3% for the others. Within the Qwen family the larger model responds more to the instruction; the two other 1.5B models fall in between. B. RQ2: does the change follow the requirement? For the core tag, the shift is +9.8 points on securityrelevant requirements and +11.2 on the others (Table III). The interaction is −1.4 points with a CI of −5.2 to +2.4, so we find no evidence that the shift depends on whether

the requirement concerns security. The interval is wide, and a moderate difference in either direction cannot be ruled out. The interactions for validation, memory, threat and prevention also include zero. Secrets and access behaves differently. On other requirements it barely moves (3.0% to 2.9%). On security-relevant ones it rises from 13.3% to 16.6%. The interaction is +3.3 points (CI 0.2 to 6.6), small but the only one that excludes zero. The one category tied to specific nouns (password, token, permission) is the one where the models respond to the requirement as well as to the prompt. C. RQ3: how complete is the generated code? More than a quarter of the generated functions are stubs (Fig. 4): 27.8% under the general prompt (CI 25.1 to 30.6) and 28.5% under the secure prompt (CI 25.9 to 31.0). Most stubs are empty bodies (18.2% of all functions); output-only and placeholder bodies make up the rest. Another 17.3% of functions are minimal, so only 51% (general) and 58% (secure) contain recognisable logic. The secure prompt does not clearly reduce stubs for any model; the per-model intervals for the two prompts overlap. OpenCoder produces stubs for about half of its functions under it (40.9% to 49.2%). Qwen 3B produces fewer empty bodies but more placeholder-marked ones (4.8% to 9.9%), the kind that say “in a real implementation” where the logic should be. The assembled files tell the same story. Compile rates are low for all models (1% to 22% of the 166 sections), and no model’s compile rate differs between prompts beyond its interval. Few sections are usable (compile, and every planned function has a non-stub body): 13.9% and 12.7% for

Qwen 3B, 5.4% and 6.6% for Qwen 1.5B, 6.0% and 3.6% for OpenCoder, and 1.2% and 0% for DeepCoder (general and secure). We also ran cppcheck 2.19.0 (warning, style, performance and portability checks, C++17, 30 seconds per file) on every assembled file. It could not parse 236 of the 653 files under the general prompt and 256 of 657 under the secure prompt, which are mostly files that do not compile. In the usable sections it reports at least one finding in 7 of 44 files under the general prompt and 10 of 38 under the secure prompt. All of these are style or performance notes, such as useStlAlgorithm and unreadVariable, and none is an error or a warning, so cppcheck gives no security signal that separates the prompts. Static analysis alone is known to understate the memory-safety risk of generated C++ [10]. The prompt changes the reasoning, but we see no clear change in how many functions are stubs or how many files compile. The plan call asks for the shared types the functions exchange, which amounts to a minimal domain model of the requirement. The small models rarely provide one. Qwen 1.5B and 3B declare no shared types for any section under either prompt, OpenCoder for at most 2% of sections, and DeepCoder for 24% to 27%. The functions then use types such as Voucher or ResourceInfo that are never defined. Among sections that fail to compile, the first compiler error is an undeclared type or name in 68% to 70% of cases for Qwen 1.5B, 51% to 54% for Qwen 3B and 39% to 51% for OpenCoder, and 18% to 19% for DeepCoder, which fails mostly on syntax. Generating from SRS text alone, without a domain model or design artifacts, leaves the models to invent the data their functions work on, and they mostly do not. Neither headline result depends on the source of the document. The core shift is +8.6 points (CI 6.8 to 10.4) on the 104 sections of source I and +9.8 points (CI 7.8 to 12.0) on the 62 of source U, and the stub rate is 27.9% and 29.3% (general and secure) for I against 27.7% and 27.2% for U. Nor does either result depend on one document. Leaving out each of the eleven documents in turn, the core shift of RQ1 (echo removed) stays between +8.8 and +9.4 points, against +9.1 with all documents, and the stub rate stays between 26.8% and 29.2% under either prompt. D. RQ4: does the code follow the reasoning? Table IV shows the share of functions whose body matches the lexical check pattern, split by whether the reasoning mentioned a check. Over all 1,982 and 2,020 functions, this share rises from 22.9% to 39.2%. A mention predicts a check in the code under both prompts, and the secure prompt raises the rate in both groups, more for functions whose reasoning mentions one: 33.5% (CI 29.0 to 38.3) to 49.9% (CI 46.1 to 53.8), a rise of 16.4 points (CI 11.3 to 21.5), against 12.9% to 16.7% (+3.8). The gap between the groups widens from 20.6 (CI 15.9 to 25.4) to 33.3 points (CI 28.7 to 37.9), a widening of 12.7 points (CI 6.4 to 19.0). The widening appears for each model, though the per-model intervals are wide. The remainder matters more for anyone reading the reasoning. Under the secure prompt, 50.1% of the functions whose

Stub Qwen 3B, general

23

Logic

Minimal

25

52

Qwen 3B, secure

19

Qwen 1.5B, general

19

24

57

Qwen 1.5B, secure

20

20

60

11

OpenCoder 1.5B, general

70

41

OpenCoder 1.5B, secure

17 49

DeepCoder 1.5B, general

30

DeepCoder 1.5B, secure

40

19

29

0

43 11 51

12

20

59

40

60

80

100

% of generated functions

Fig. 4. Share of generated functions that are stubs (empty, output or trivial only, or placeholder), minimal, or contain recognisable logic, by model and prompt. Heuristic classes; Section VI reports a hand check of the stub flag. Reasoning (4 steps, abridged) 1 The function should check if the HTML content of a website is valid . . . by parsing the HTML content and ensuring that it is well-formed. 2 To validate the HTML content, we can use a library such as libxml2 or pugixml. 3 The function should also check if the HTML content contains any harmful content . . . by scanning for specific keywords or patterns. 4 To check for harmful content, we can use a library such as libcurl or libxml2. Code bool validate_website_content(const std::vector<std::string >& content) { // Parse the HTML content using a library such as libxml2 or pugixml // Validate the HTML content using a library such as libcurl or libxml2 // Check for harmful content using a library such as libcurl or libxml2 return true; // Return true if the HTML content is valid and does not contain harmful content }

Fig. 5. Reasoning and code for one function (Qwen 1.5B, secure prompt, video search SRS, purpose “Validates the HTML content of a website”). The code is verbatim.

reasoning mentions a check have none that our pattern finds. Under the general prompt the figure is 66.5%. These counts already exclude empty and placeholder bodies; among all functions whose reasoning mentions a check, including stubs (1,128 and 1,584), 17.7% (general) and 20.1% (secure) are stubs by the RQ3 classes. Functions whose reasoning says nothing about a check still contain one 16.7% of the time under the secure prompt, so silence in the reasoning is not strong evidence of absence either. Fig. 5 shows a typical case. Asked under the secure prompt to validate the HTML content of a website, Qwen 1.5B reasons about parsing, validation and scanning for harmful content, names two libraries, and returns a body that consists of comments and return true. The function compiles, and a reader who trusts the reasoning would assume it is checked. E. RQ5: does compiler feedback make the code usable? Fig. 6 shows the three rounds, pooled over Qwen 1.5B, Qwen 3B and OpenCoder (498 model–section cases per

TABLE IV S HARE OF FUNCTIONS WITH A CHECK IN THE CODE , BY WHETHER THE REASONING MENTIONS ONE . F UNCTIONS WITH A NON - EMPTY BODY AND AT LEAST ONE REASONING STEP ; A CHECK IS A MATCH OF THE LEXICAL PATTERN IN S ECTION III-C. n IN PARENTHESES .

Usable sections (%)

Scope

Prompt

Mentions

No mention

Gap

20

All

General Secure

33.5 (966) 49.9 (1372)

12.9 (1016) 16.7 (648)

20.6 33.3

10

General Secure General Secure General Secure General Secure

37.6 (213) 57.7 (300) 37.6 (141) 49.7 (163) 29.0 (276) 33.8 (317) 33.0 (336) 54.7 (592)

7.3 (137) 17.6 (68) 16.5 (273) 16.8 (190) 13.6 (295) 14.9 (255) 11.6 (311) 19.3 (135)

30.3 40.0 21.1 32.9 15.4 18.9 21.5 35.5

DeepCoder OpenCoder Qwen 1.5B Qwen 3B

prompt). Repair helps. Under the general prompt the share of usable sections rises from 8.4% (CI 6.0 to 11.2) after the first generation to 14.1% after C1 and 17.5% (CI 14.1 to 21.3) after C2. Under the secure prompt it rises from 7.6% to 11.7% and 13.9% (CI 10.6 to 17.3). Most of the gain comes from filling stubs: the share of planned functions that are stubs or missing falls from 28.1% to 16.5% (general) and from 29.3% to 18.0% (secure). The second round adds less than the first. Repair fixes compile errors much less reliably. The share of sections that compile rises from 16.5% to 20.5% under the general prompt and does not move under the secure prompt (16.9% to 17.1%). For OpenCoder it falls with each round (from 33 to 24 sections under the general prompt), because reimplementing a stub can break a file that compiled before, and the compile round keeps the new version. Qwen 3B benefits most: under the general prompt its usable sections go from 23 to 47 of 166. After two rounds more than 80% of sections are still unusable under either prompt. The secure prompt does not catch up. Its usable share is 0.8 points below the general prompt after the first generation (CI −3.2 to +1.8), 2.4 points below after C1 and 3.6 points below after C2 (CI −7.6 to 0.0). The gap grows in each round but its interval still reaches zero, so we read it as no benefit rather than harm. DeepCoder gains almost nothing from two repair rounds. Of 166 sections, usable ones go from 2 to 4 to 5 under the general prompt and from 0 to 0 to 1 under the secure prompt. Sections that compile go from 5 to 5 to 6 (general) and from 1 to 0 to 1 (secure). Most of its sections fail on malformed output or syntax errors (RQ3), which repair rarely fixes. F. Exploratory bounded model checking of usable code Formal verification has been used to analyse large sets of AI-generated C programs [21]. We ran ESBMC 8.0.0 [22] on the usable sections, one function at a time (--function), so the checks cover only the sections that compile and have no stub, 6% of all runs in R0, 10% after C1 and 12% after C2. ESBMC checks array bounds, pointers and division by zero by default; we added the memory-leak and overflow checks, a

Secure prompt

General prompt

Stub or missing functions (%) 30 20 10

0

R0

C1

0

C2

R0

C1

C2

Fig. 6. Compile repair, pooled over Qwen 1.5B, Qwen 3B and OpenCoder. Left: share of model–section cases that are usable. Right: share of planned functions that are stubs or missing. Bars are 95% bootstrap intervals over requirement sections. R0 is the first generation; C1 and C2 are repair rounds with compiler feedback. TABLE V ESBMC VERDICTS PER FUNCTION ON USABLE SECTIONS , POOLED OVER THE FOUR MODELS . R0 IS THE FIRST GENERATION , AND C1 AND C2 FOLLOW ONE AND TWO COMPILE - REPAIR ROUNDS . V IOLATIONS ARE SPLIT BY WHERE ESBMC PLACES THE VIOLATED PROPERTY: IN THE GENERATED CODE OR INSIDE ITS C++ LIBRARY MODELS . T HE TWO PROMPTS ARE CHECKED ON DIFFERENT SETS OF FUNCTIONS , BECAUSE THEIR USABLE SECTIONS DIFFER . Violation Round Prompt Funcs Verified Code Library Timeout Unsupp. R0

General Secure

155 138

49 40

17 10

51 45

4 2

34 41

C1

General Secure

274 208

94 51

21 16

79 66

18 14

62 61

C2

General Secure

340 261

120 62

28 17

88 91

29 14

75 77

loop unwinding bound of 8 and a 30-second limit per function. Function arguments are unconstrained, so a violation shows that some input breaks the function, not that the program as a whole is reachable that way. Each function gets one verdict: verified (no violation within the bound), violation, timeout, or unsupported (ESBMC’s C++ frontend failed before checking). ESBMC could not parse <optional> next to its own C++ library models, so we remove that include from a temporary copy of each file. For every violation we also rerun ESBMC and record whether the violated property lies in the generated code or inside ESBMC’s built-in library models. We treat this run as exploratory. We did not triage the violations, so each one is a lead to inspect, not a confirmed defect. Tab. V gives the counts for the first generation (R0) and after each repair round (C1, C2). Of the 293 functions checked in R0, 89 (30%) verified, 123 (42%) had a violation, 6 timed out and 75 (26%) were unsupported. Of the 601 checked after C2, 182 (30%) verified, 224 (37%) had a violation, 43 (7%) timed out and 152 (25%) were unsupported. The shares barely change with repair. Most violations do not point at the generated code. ESBMC places 96 of the 123 violations in R0 (78%), 145 of 182 in C1

(80%) and 179 of 224 in C2 (80%) inside its library models. They are mainly dereference failures reported as incorrect alignment or invalid pointer inside the string and map models. We do not count them as defects in the generated code, and we did not inspect them one by one. The remaining violations, 27 in R0 and 45 after C2, lie in the generated code: arithmetic overflow on multiplication and on floating-point addition, and some dereference failures. We did not triage these either, and with unconstrained arguments some may not be reachable in the program. Per checked function, the secure prompt has fewer violations in the generated code than the general prompt (10 of 138, 7.2%, against 17 of 155, 11.0%, in R0; 17 of 261, 6.5%, against 28 of 340, 8.2%, after C2). The counts are small, the function sets differ, and we did not test the difference, so we do not read it as an effect. A quarter of the functions are unsupported, and the cause is mostly the C++ standard library. ESBMC replaces the library with its own simplified models, and generated code often calls members these lack. In a sample of 60 unsupported functions from R0, the first frontend error was a call ESBMC could not match for std::string::insert, find or substr in 40 cases, a std::set<std::string> constructor in 5 and a std::isalnum or std::isprint call in 9. Structured bindings, undefined template instantiations and overloaded operators account for further failures. Functions whose name --function cannot select, mostly overloaded names, add 16 more after C2. Verified means no violation within the unwinding bound and the time limit, not that the function is safe, and 2% to 7% of the checks timed out. Because unsupported functions are dropped and library-model violations are set aside, the verdicts describe a subset of the code that is itself a small part of everything generated. V. D ISCUSSION The prompt changes the reasoning more clearly than the code. Across four models, a two-line security instruction more than doubles the security content of the reasoning and raises the share of analysed functions with a lexically recognised check from 23% to 39%. We see no clear change in the share of stubs, in compile rates or in usability. The model writes more checking language and more lexically recognised checks, but not fewer stubs. The reasoning still misleads often: among functions whose reasoning mentions a check, half contain no check our pattern recognises under the secure prompt. The tools do not contradict this. On the usable code, cppcheck finds only style and performance notes under either prompt, and the exploratory ESBMC run reports a few in-code violations under both. The checked sets are small and differ between prompts, so we do not claim there is no difference. We found no clear evidence that the response was more targeted toward security-relevant requirements. For example, the shift is not clearly larger for a requirement about passwords or access than for one not classified as security-relevant, and the reasoning becomes more conditional and less concrete. Both fit a model that adds cautionary language whenever it is told to be careful, rather than one that reasons about the risks

of the requirement in front of it. The selective rise for secrets and access, the one category tied to specific nouns, suggests that the requirement text does matter when it gives the model a concrete hook. A prompt that names the specific risks of each task is a candidate we have not tested. Stubs are a limit of small models in requirements-to-code generation. More than a quarter of the functions are empty, output-only or placeholder bodies, and fewer than six in ten contain recognisable logic. These pooled patterns occur under both prompts, although the proportions vary substantially by model; OpenCoder produces stubs for about half of its functions. Requirements written for people leave out the data structures, interfaces and surrounding system that an implementation needs, and the small models in our study fill that gap with empty or placeholder bodies rather than with assumptions they then implement. For practitioners, a small model’s output for an SRS section is closer to a skeleton than to an implementation, and the security reasoning attached to it should be read in that light. These symptoms may share one cause: we skip the design step. Stubs, undeclared types and files that do not compile are what we would expect when a model must invent the data model and the function interfaces while it writes code. We did not test this. A condition in which the model first produces a domain model or class diagram, as in Wei’s stepwise method, would show whether the design step reduces them. The repair loop helps but does not rescue. Feeding compiler errors back is the cheapest agentic step one can add, and it does recover a share of the code: usable sections roughly double over two rounds, mainly because missing and empty functions get written. It does not fix most compile failures, and the gains shrink from the first round to the second. Many failures come from types the plan never declared. For small models, a repair loop is worth running but should be paired with a design step that fixes the data model first. Static analysis and model checking cover little of the generated code. cppcheck cannot parse more than a third of the files. ESBMC checks only the usable sections, cannot parse a quarter of those because its C++ library models lack members the code calls, and places most of the violations it reports inside those models. For generated C++ that uses the standard library, model checker verdicts need manual inspection before they can count as evidence about the code. A reviewer who sees “validate the input, check for null and bounds” will assume the function does so. In our data it often does not: half of the functions whose reasoning mentions a check contain no check our lexical pattern recognises under the secure prompt, and two thirds under the general prompt. A workflow that shows reasoning to people should show the code-level evidence next to it, or check the claim mechanically. Follow-through of the kind we measure is cheap to compute and could serve as a gate before a function is accepted. In a planner–implementer split, the plan call sees the same prompt as the function call. If a security instruction is meant to change the code, it may need to act on the plan (which checks exist as functions, which inputs are untrusted) and

TABLE VI H AND CHECK ON THE BLIND SAMPLES (150 STEPS , 100 FUNCTIONS ). AUTO , H1 AND H2 ARE THE NUMBERS OF ITEMS MARKED POSITIVE BY THE AUTOMATIC LABEL ( REVISED KEYWORD LISTS ) AND BY ANNOTATORS H1 AND H2. κ IS C OHEN ’ S KAPPA BETWEEN H1 AND H2. P RECISION AND RECALL ARE OF THE AUTOMATIC LABEL AGAINST H1 / H2; A DASH MEANS NO ITEM TO DIVIDE BY. T HE CORE ROW IS THE UNION OF VALIDATION , MEMORY, THREAT AND PREVENTION , WITH ECHO WORDING REMOVED FROM THE AUTOMATIC TAGS . T HE STUB ROW COVERS THE 100 FUNCTIONS . Auto H1 H2

κ

Precision

Recall

validation memory/resources threat prevention echo core (4 tags, no echo)

19 33 42 0 4 5 0 0 4 1 2 2 3 5 1 19 38 48

0.84 0.89 0.00 1.00 0.33 0.84

0.74 / 0.84 –/– –/– 1.00 / 1.00 0.67 / 0.33 0.79 / 0.89

0.42 / 0.38 0.00 / 0.00 – / 0.00 0.50 / 0.50 0.40 / 1.00 0.39 / 0.35

stub function

60 43 57 0.73 0.65 / 0.82 0.91 / 0.86

Label

on a verification step, since reasoning at implementation time comes late and is not reliable. VI. T HREATS TO VALIDITY Measurement. The content tags, the stub classes and the check-in-code pattern are lexical heuristics. Two annotators labelled a blind sample of 150 reasoning steps (balanced across prompts) and 100 functions (20 per heuristic class) independently, with a written protocol and without seeing the model, prompt or automatic label. H1, a second-year computer science doctoral student, needed about 3 hours for the steps and 2.5 for the functions; H2, a software engineering graduate student, needed 3.5 and 2. We did not adjudicate their labels. The annotators agree well on validation, memory, prevention, the core union and the stub flag (κ 0.73 to 1.00), and less on whether a function implements its purpose (κ 0.58). The check exposed generic words in our first keyword lists (ensure, robust, secure, safe, and bare pointer, resources and null): prevention flagged 18 steps and each annotator accepted 2, and neither accepted any of the 3 memory or 3 threat hits. We removed these words, so the revised precision in Tab. VI is optimistic. The revised core is precise (0.79 and 0.89) but misses more than half of the annotators’ positives (recall 0.39 and 0.35). Memory and threat are too rare to validate on 150 random steps, which would hold about three and two hits. The stub flag over-counts (precision 0.65 and 0.82, recall 0.91 and 0.86). On the sample, both annotators see a larger secure-minus-general shift than the automatic core (+26.7 and +24.0 points against +9.3). The sample is too small to tell whether this holds in general. We did not check the followthrough measure by hand; it tests whether a function has some recognised check, not the one the reasoning names. The relevance split uses a coarse term list. Reasoning. The reasoning is text the model writes in a JSON field before the code, not a record of how the code was produced. We claim only that it does not predict the code well enough to serve as evidence about it. We store DeepCoder’s native thinking trace but do not analyse it.

Sampling and models. We ran one greedy sample per section and prompt. DeepCoder’s pairs are a subset because of malformed output. The study covers four code-specialized models of 1.5B to 3B parameters and C++ only, and the two prompts differ in length as well as content. Outcomes and input. Low compile rates limit the codelevel comparison. Repair uses compiler feedback only. The ESBMC run is exploratory, untriaged and limited to usable sections; other analysers may report other issues. The models see only the SRS text of one section, with no design artifacts. Data. We use eleven of the eighteen PURE documents available in XML, balanced by source. PURE leans towards documents with a high level of abstraction [18], and larger documents weigh more in the pooled results. VII. C ONCLUSION We compared the reasoning and code of four small code models generating C++ from software requirements under a general and a secure prompt. The secure prompt more than doubles the security content of the reasoning, with no evidence of a larger rise for security-relevant requirements, and makes the reasoning less specific. The code changes only in part. Among functions with a body and reasoning, the share with a lexically recognised check rises from 23% to 39%, but more than a quarter of all functions are stubs under either prompt, and compile and usability rates show no clear difference. Half of the functions whose reasoning mentions a check contain no recognised check under the secure prompt, and two thirds under the general prompt. Two rounds of compiler-feedback repair roughly double the usable share but leave more than 80% of sections unusable, and the secure prompt does not catch up. cppcheck and an exploratory ESBMC run do not show a clear difference between the prompts on the usable code, and ESBMC cannot check a quarter of it. A hand check by two annotators supports the stub measure and led us to revise three keyword lists that matched generic words. The revised reasoning measure is precise but misses more than half of what the annotators mark. Both annotators see the same direction. For small models in agentic requirements-to-code workflows, a security instruction changes the reasoning text and adds some checking code, but we see no clear reduction in stubs, and the reasoning should be checked against the code rather than trusted. We ran one greedy sample per section, the hand check covers 150 steps and 100 functions, and the reasoning measures are lexical, so the numbers show direction more than size. Open work is adjudicating the labels, analyserdriven security repair, a larger model, and a design step and prompts naming task-specific risks. DATA AVAILABILITY the PURE XML documents, the requirement sections extracted from them, and the list of the 166 sections used; • the generated code, reasoning and plans for the first generation and both repair rounds (R0, C1, C2), one folder per prompt and model; • the tagged reasoning, result tables and analyser outputs; •

the blind label sheets, the key files with the automatic labels, both annotators’ labels and the labelling protocol; • the scripts and a README with the commands.

•

R EFERENCES [1] H. Pearce, B. Ahmad, B. Tan, B. Dolan-Gavitt, and R. Karri, “Asleep at the keyboard? Assessing the security of GitHub Copilot’s code contributions,” vol. 68, no. 2. ACM New York, NY, USA, 2025, pp. 96–105. [2] J. He and M. Vechev, “Large language models for code: Security hardening and adversarial testing,” in Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, 2023, pp. 1865–1879. [3] M. Turpin, J. Michael, E. Perez, and S. Bowman, “Language models don’t always say what they think: Unfaithful explanations in chainof-thought prompting,” Advances in Neural Information Processing Systems, vol. 36, pp. 74 952–74 965, 2023. [4] T. Lanham, A. Chen, A. Radhakrishnan, B. Steiner, C. Denison, D. Hernandez, D. Li, E. Durmus, E. Hubinger, J. Kernion et al., “Measuring faithfulness in chain-of-thought reasoning,” arXiv preprint arXiv:2307.13702, 2023. [5] N. Perry, M. Srivastava, D. Kumar, and D. Boneh, “Do users write more insecure code with ai assistants?” in Proceedings of the 2023 ACM SIGSAC conference on computer and communications security, 2023, pp. 2785–2799. [6] G. Sandoval, H. Pearce, T. Nys, R. Karri, S. Garg, and B. Dolan-Gavitt, “Lost at c: A user study on the security implications of large language model code assistants,” in 32nd USENIX Security Symposium (USENIX Security 23), 2023, pp. 2205–2222. [7] R. Khoury, A. R. Avila, J. Brunelle, and B. M. Camara, “How secure is code generated by chatgpt?” arXiv preprint arXiv:2304.09655, 2023. [8] C. Tony, M. Mutas, N. E. D. Ferreyra, and R. Scandariato, “Llmseceval: A dataset of natural language prompts for security evaluations,” in 2023 IEEE/ACM 20th international conference on mining software repositories (MSR). IEEE, 2023, pp. 588–592. [9] M. Bhatt, S. Chennabasappa, C. Nikolaidis, S. Wan, I. Evtimov, D. Gabi, D. Song, F. Ahmad, C. Aschermann, L. Fontana et al., “Purple llama cyberseceval: A secure coding benchmark for language models,” arXiv preprint arXiv:2312.04724, 2023. [10] S. Mahmud, F. Sikder, Y. Ji, H. Zhang, and Y. Lei, “The illusion of safety: Multi-tier verification of AI vs. human C++ code,” arXiv:2607.00107, 2026.

[11] J. Wei, X. Wang, D. Schuurmans, M. Bosma, F. Xia, E. Chi, Q. V. Le, D. Zhou et al., “Chain-of-thought prompting elicits reasoning in large language models,” Advances in neural information processing systems, vol. 35, pp. 24 824–24 837, 2022. [12] S. Wiegreffe, A. Marasović, and N. A. Smith, “Measuring association between labels and free-text rationales,” in Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, 2021, pp. 10 266–10 284. [13] S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y. Cao, “ReAct: Synergizing reasoning and acting in language models,” arXiv:2210.03629, 2023. [14] C. E. Jimenez, J. Yang, A. Wettig, S. Yao, K. Pei, O. Press, and K. Narasimhan, “Swe-bench: Can language models resolve real-world github issues?” in International Conference on Learning Representations, vol. 2024, 2024, pp. 54 107–54 157. [15] X. Chen, M. Lin, N. Schärli, and D. Zhou, “Teaching large language models to self-debug,” in International Conference on Learning Representations, vol. 2024, 2024, pp. 8746–8825. [16] B. Wei, “Requirements are all you need: From requirements to code with llms,” in 2024 IEEE 32nd International Requirements Engineering Conference (RE). IEEE, 2024, pp. 416–422. [17] P. Belcak, G. Heinrich, S. Diao, Y. Fu, X. Dong, S. Muralidharan, Y. C. Lin, and P. Molchanov, “Small language models are the future of agentic ai,” arXiv preprint arXiv:2506.02153, 2025. [18] A. Ferrari, G. O. Spagnolo, and S. Gnesi, “Pure: A dataset of public requirements documents,” in 2017 IEEE 25th international requirements engineering conference (RE). IEEE, 2017, pp. 502–505. [19] B. Hui, J. Yang, Z. Cui, J. Yang, D. Liu, L. Zhang, T. Liu, J. Zhang, B. Yu, K. Lu et al., “Qwen2. 5-coder technical report,” arXiv preprint arXiv:2409.12186, 2024. [20] S. Huang, T. Cheng, J. K. Liu, W. Xu, J. Hao, L. Song, Y. Xu, J. Yang, J. Liu, C. Zhang et al., “Opencoder: The open cookbook for top-tier code large language models,” in Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), 2025, pp. 33 167–33 193. [21] N. Tihanyi, T. Bisztray, R. Jain, M. A. Ferrag, L. C. Cordeiro, and V. Mavroeidis, “The FormAI dataset: Generative AI in software security through the lens of formal verification,” in Proceedings of the 19th international conference on predictive models and data analytics in software engineering, 2023, pp. 33–43. [22] M. R. Gadelha, F. R. Monteiro, J. Morse, L. C. Cordeiro, B. Fischer, and D. A. Nicole, “Esbmc 5.0: an industrial-strength c model checker,” in Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018, pp. 888–891.

Related documents

Record · ID 1605335 · SHA-256 b5f8b54a76b180df
Retrieved via Conceptio: every document is proof-bundled with source, license, and retrieval metadata.
Bring this data into your agent: Connect via MCP or API · 20 free credits to start · no card required
Read the Docs → · View CLI source on GitHub · Conceptio Open Knowledge Archive