pith. sign in

arxiv: 2605.21532 · v1 · pith:CIHSYREYnew · submitted 2026-05-19 · 💻 cs.PL · cs.SE

Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code

Jesper Amilon , Merlijn Sevenhuijsen , Mattias Nyberg , Karl Palmskog This is my paper

Pith reviewed 2026-05-22 00:58 UTC · model grok-4.3

classification 💻 cs.PL cs.SE
keywords non-functional requirementsC codeFrama-C pluginembedded systemssafety-criticalmodule contractsautomotive softwarecontrol flow verification
0
0 comments X

The pith

A Frama-C plugin verifies non-functional requirements in safety-critical C code using module contracts

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper establishes a set of general rules for non-functional requirements in C code for safety-critical embedded automotive systems. The rules focus on modules and their interfaces and are designed to be orthogonal to existing standards like MISRA-C. An interface specification contract language is proposed to specify these requirements, and a checker is implemented as a Frama-C plugin that examines control flow and data flow properties. This enables verification that only permitted functions are called and variables are properly initialized, addressing risks from untrusted code sources. The approach is demonstrated through case studies on real C code from Scania trucks, integrated with functional ACSL contracts.

Core claim

The authors introduce general rules for non-functional requirements centered on modules and interfaces in safety-critical C code, along with an interface contract language and a Frama-C plugin that checks the rules by analyzing control and data flows to ensure safe module interactions, such as restricting calls to permitted functions.

What carries the argument

An interface specification contract language for C modules that defines permitted interactions, which the Frama-C plugin uses to enforce non-functional properties like control flow restrictions and data initialization.

If this is right

  • Verification of untrusted code from various sources becomes feasible alongside functional checks.
  • The rules complement rather than replace popular C coding standards.
  • A complete toolchain supports both module contracts and ACSL function contracts.
  • Real-world applicability is shown in automotive software case studies.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The method may help verify code generated by large language models for embedded use.
  • It opens possibilities for checking safe composition of modules from different developers.
  • Further rules could be added to cover more properties like memory safety or timing constraints.

Load-bearing premise

The chosen non-functional rules are necessary and sufficient to prevent unsafe behavior in untrusted C code for these systems.

What would settle it

Running a verified module in the actual embedded environment and observing an unsafe function call or uninitialized variable access that the checker failed to detect.

Figures

Figures reproduced from arXiv: 2605.21532 by Jesper Amilon, Karl Palmskog, Mattias Nyberg, Merlijn Sevenhuijsen.

Figure 1
Figure 1. Figure 1: ECU architecture with internal and external interactions. [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Example C function annotated with an ACSL contract. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Module Interface Specification (IS) contract [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Implementations of the timed monitor (tmon) module from Figure 3. [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Grammar for module IS contracts. 4.1 Running example The IS contract in [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Proposed module development and verification workflow and toolchain [PITH_FULL_IMAGE:figures/full_fig_p013_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Excerpt of the IS contract for SFLD. 7.1 Specification and verification approach To run the toolchain on each module, we first wrote ACSL specifications and IS contracts, based on existing requirement documents in natural language written by engineers. The ACSL specifications consist of function contracts for each entry-point function. We also wrote ACSL contracts for the external functions that are permit… view at source ↗
Figure 8
Figure 8. Figure 8: Excerpt of the IS contract for SGMM. flow diagram, and five requirements expressed as pseudo-code. The control flow diagram and the five requirements both express the conditions under which the module should ensure that the magnetic valves are blocked [PITH_FULL_IMAGE:figures/full_fig_p017_8.png] view at source ↗
read the original abstract

Code contracts provide a robust way to specify functional requirements of safety-critical software in embedded systems. For example, the ANSI/ISO C Specification Language (ACSL) can be used to specify the functional behavior of C code that is then formally verified by the Frama-C framework's Wp plugin. However, non-functional requirements, such as restrictions on control flow and data flow, are also important for embedded systems safety. Untrusted code developed by subcontractors, junior developers, or generated by large language models, can be verified by Wp but may nevertheless call unsafe functions or use uninitialized program variables. To address this problem, we constructed a set of general rules concerning non-functional requirements of C code in safety-critical embedded systems. Our rules are orthogonal to popular C rulesets such as MISRA-C and center on modules and their interaction through interfaces. To enable checking our rules, we propose an interface specification contract language for C modules. We implemented a checker for our rules as a Frama-C plugin, which takes as input a C module and its contract and checks control flow and data flow properties, ensuring, e.g., that only permitted functions are called by the module. We integrated our checker in a toolchain to enable specification and verification of module contracts and ACSL contracts for untrusted code. We report on two case studies on safety-critical C code using software in Scania trucks, where we defined module contracts and ACSL function contracts based on informal system requirements and verified them using our toolchain.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper claims to construct a set of general rules for non-functional requirements (e.g., permitted function calls, initialized variables) in safety-critical embedded C code that are orthogonal to MISRA-C and focus on modules and interfaces; it proposes an interface specification contract language, implements a Frama-C plugin that checks control- and data-flow properties against module contracts, integrates the checker with ACSL/Wp for combined functional and non-functional verification, and evaluates the toolchain on two case studies using safety-critical C code from Scania trucks.

Significance. If the central claims hold, the work fills a practical gap in verifying untrusted or generated code in automotive embedded systems by adding enforceable non-functional constraints that complement existing functional contract tools. The industrial case studies and toolchain integration provide concrete evidence of applicability; the orthogonality to MISRA-C and focus on module interfaces are potentially reusable contributions to the broader area of contract-based verification for C.

major comments (2)
  1. [plugin implementation / contract language] Plugin implementation and contract language sections: no formal semantics is given for the proposed interface specification contract language, and no soundness argument or proof is provided that the Frama-C plugin correctly and completely detects all violations of the stated control- and data-flow rules on arbitrary C code. This is load-bearing for the claim that the checker 'ensures' compliance (e.g., that only permitted functions are called), especially given common embedded C features such as pointers, aliasing, function pointers, and volatile variables that are not addressed in the described checks.
  2. [case studies] Case studies section: the two industrial examples are presented at a high level with no quantitative results (number of rules checked, violations found or missed, false-positive rate, coverage of C constructs, or comparison against manual review). Without these data it is impossible to assess whether the plugin actually enforces the rules in practice or to evaluate the central claim that the approach works for real safety-critical automotive code.
minor comments (2)
  1. [abstract / introduction] The abstract and introduction should explicitly list the concrete non-functional rules that were formalized (permitted calls, initialization, etc.) rather than describing them only at the level of 'control flow and data flow properties'.
  2. [contract language] Notation for the interface contract language is introduced without a grammar or BNF; a small example contract together with the corresponding C module would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed feedback. We address the major comments point by point below, indicating planned revisions to improve the manuscript.

read point-by-point responses

  1. Referee: Plugin implementation and contract language sections: no formal semantics is given for the proposed interface specification contract language, and no soundness argument or proof is provided that the Frama-C plugin correctly and completely detects all violations of the stated control- and data-flow rules on arbitrary C code. This is load-bearing for the claim that the checker 'ensures' compliance (e.g., that only permitted functions are called), especially given common embedded C features such as pointers, aliasing, function pointers, and volatile variables that are not addressed in the described checks.

    Authors: We agree that the absence of a formal semantics and soundness proof is a limitation for the stronger claims of the work. The contract language and rules were developed from practical requirements in automotive embedded systems and implemented directly in the Frama-C plugin using its existing control- and data-flow analyses. We will revise the relevant sections to provide an informal semantics for the contract language, clarify the scope of the checks, and explicitly discuss limitations with respect to pointers, aliasing, function pointers, and volatile variables. We will also adjust the wording from 'ensures' to 'checks compliance with' to better reflect the practical, tool-supported nature of the approach. revision: yes

  2. Referee: Case studies section: the two industrial examples are presented at a high level with no quantitative results (number of rules checked, violations found or missed, false-positive rate, coverage of C constructs, or comparison against manual review). Without these data it is impossible to assess whether the plugin actually enforces the rules in practice or to evaluate the central claim that the approach works for real safety-critical automotive code.

    Authors: The case studies were chosen to show applicability to real safety-critical Scania truck codebases. We will expand the section to report quantitative details that were collected during the experiments, including the number of non-functional rules checked per module, the number of violations identified, and the extent of code coverage by the checks. A controlled false-positive rate study or direct comparison to manual review was not performed, as the verification was carried out within an industrial workflow; we will therefore report only the metrics that are available and discuss the observed practical outcomes. revision: partial

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained implementation and case study

full rationale

The paper constructs a new set of non-functional rules for C modules in safety-critical systems, proposes an interface contract language, implements a Frama-C plugin for control/data-flow checks, and evaluates via two case studies on Scania truck code. These steps are presented as direct engineering contributions orthogonal to MISRA-C and integrated with ACSL/Wp, without any reduction of claims to self-citations, fitted parameters renamed as predictions, definitional equivalences, or load-bearing uniqueness theorems from prior author work. The central claims rest on the described toolchain and informal-to-formal mapping rather than circular reuse of inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The approach rests on domain assumptions about what counts as a non-functional requirement in safety-critical embedded C and on the correctness of the underlying Frama-C framework. No free parameters or invented physical entities are introduced.

axioms (2)
  • domain assumption Non-functional requirements such as restrictions on control flow and data flow can be captured by module-level interface contracts that are orthogonal to existing functional specification languages like ACSL.
    Stated in the abstract when the authors describe constructing general rules and proposing the contract language.
  • domain assumption A static checker implemented as a Frama-C plugin can reliably detect violations of these rules in real C code.
    Implicit in the claim that the plugin checks control flow and data flow properties and was used successfully in case studies.

pith-pipeline@v0.9.0 · 5809 in / 1581 out tokens · 37664 ms · 2026-05-22T00:58:27.050620+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages · 2 internal anchors

  1. [1]

    Amilon et al

    Abella, J., Hernandez, C., Quiñones, E., Cazorla, F.J., Conmy, P.R., Azkarate- askasua, M., Perez, J., Mezzetti, E., Vardanega, T.: WCET analysis methods: Pit- 22 J. Amilon et al. falls and challenges on their trustworthiness. In: International Symposium on In- dustrial Embedded Systems. pp. 1–10 (2015). https://doi.org/10.1109/SIES.2015. 7185039

    work page doi:10.1109/sies.2015 2015

  2. [2]

    The Llama 3 Herd of Models

    AI@Meta: The llama 3 herd of models. arXiv preprint arXiv:2407.21783 (2024), https://arxiv.org/abs/2407.21783

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  3. [3]

    com/bedrock/ (2026), accessed: 2026-04-16

    AmazonWebServices:Amazonbedrockdocumentation.https://docs.aws.amazon. com/bedrock/ (2026), accessed: 2026-04-16

    work page 2026

  4. [4]

    Huennefeld, W

    Amilon, J.: Vernfr for isola 2026 (Apr 2026). https://doi.org/10.5281/zenodo. 19706522, https://doi.org/10.5281/zenodo.19706522

    work page doi:10.5281/zenodo 2026

  5. [5]

    Amilon, J., Gurov, D., Lidström, C., Nyberg, M., Ung, G., Wingbrant, O.: Au- toDeduct: A tool for automated deductive verification of C code (2025), https: //arxiv.org/abs/2501.10889

    work page arXiv 2025

  6. [6]

    https://anthropic.com/ claude-sonnet-4-6-system-card (Feb 2026), accessed: 2026-04-16

    Anthropic: Claude sonnet 4.6 system card. https://anthropic.com/ claude-sonnet-4-6-system-card (Feb 2026), accessed: 2026-04-16

    work page 2026

  7. [7]

    Baudin, P., Bobot, F., Bühler, D., Correnson, L., Kirchner, F., Kosmatov, N., Maroneze, A., Perrelle, V., Prevosto, V., Signoles, J., Williams, N.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM64(8), 56–68 (Jul 2021). https://doi.org/10.1145/3470569

    work page doi:10.1145/3470569 2021

  8. [8]

    CEA-List (2025), https://www.frama-c.com/download/ frama-c-wp-manual.pdf, Frama-C 32.0 (Germanium)

    Baudin, P., Bobot, F., Correnson, L., Dargaye, Z., Blanchard, A.: Frama- C WP Plug-in Manual. CEA-List (2025), https://www.frama-c.com/download/ frama-c-wp-manual.pdf, Frama-C 32.0 (Germanium)

    work page 2025

  9. [9]

    Baudin, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language, https://frama-c.com/download/acsl.pdf

    work page

  10. [10]

    In: Programming Languages and Systems

    Beringer, L.: Verified software units. In: Programming Languages and Systems. pp. 118–147. Springer International Publishing, Cham (2021). https://doi.org/10. 1007/978-3-030-72019-3_5

    work page 2021

  11. [11]

    CEA-List (2025), https://www.frama-c

    Bühler, D., Cuoq, P., Yakobowski, B., Lemerre, M., Maroneze, A., Perrelle, V., Pre- vosto, V.: Frama-C Eva Plug-in Manual. CEA-List (2025), https://www.frama-c. com/download/frama-c-eva-manual.pdf, frama-C 32.0 (Germanium)

    work page 2025

  12. [12]

    In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation

    Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z.: End-to-end veri- fication of stack-space bounds for C programs. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 270–281. PLDI ’14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2594291.2594301

    work page doi:10.1145/2594291.2594301 2014

  13. [13]

    Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-Ergo 2.2 (Jul 2018), https://inria.hal.science/hal-01960203

    work page 2018

  14. [14]

    Frama-C developers: ACSL importer (2026), https://www.frama-c.com/ fc-plugins/acsl-importer.html

    work page 2026

  15. [15]

    GNU Project: Header files (2026), https://gcc.gnu.org/onlinedocs/cpp/ Header-Files.html, GCC C Preprocessor Manual, accessed 2026-03-25

    work page 2026

  16. [16]

    In: Petrucci, L., Seceleanu, C., Cavalcanti, A

    Gurov, D., Lidström, C., Nyberg, M., Westman, J.: Deductive functional verifi- cation of safety-critical embedded C-code: An experience report. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) Critical Systems: Formal Methods and Au- tomated Verification. pp. 3–18. Springer International Publishing, Cham (2017). https://doi.org/10.1007/978-3-319-67113-0_1

    work page doi:10.1007/978-3-319-67113-0_1 2017

  17. [17]

    Com- puter39(6), 95–99 (2006)

    Holzmann, G.J.: The power of 10: rules for developing safety-critical code. Com- puter39(6), 95–99 (2006). https://doi.org/10.1109/MC.2006.212

    work page doi:10.1109/mc.2006.212 2006

  18. [18]

    In: Beckert, B., Marché, C

    Huisman, M., Gurov, D.: CVPP: A tool set for compositional verification of control–flow safety properties. In: Beckert, B., Marché, C. (eds.) Formal Verifica- tion of Object-Oriented Software. pp. 107–121. Springer Berlin Heidelberg, Berlin, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18070-5_8 Contract Based Verification of Non-functional Requir...

    work page doi:10.1007/978-3-642-18070-5_8 2011

  19. [19]

    ISO: Programming languages—C (1999), ISO/IEC 9899:1999

    work page 1999

  20. [20]

    ISO: Road vehicles controller area network (CAN) (2015), ISO 11898-1:2015

    work page 2015

  21. [21]

    ISO: ISO26262: Road vehicles - functional safety 2nd ed. (2018)

    work page 2018

  22. [22]

    In: International Conference on Machine Learning

    Kambhampati, S., Valmeekam, K., Guan, L., Verma, M., Stechly, K., Bhambri, S., Saldyt, L., Murthy, A.: Position: LLMs can’t plan, but can help planning in LLM- modulo frameworks. In: International Conference on Machine Learning. ICML’24, JMLR.org (2024). https://doi.org/10.5555/3692070.3692991

    work page doi:10.5555/3692070.3692991 2024

  23. [23]

    Formal Aspects of Computing27(3), 573–609 (2015)

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

    work page doi:10.1007/s00165-014-0326-7 2015

  24. [24]

    Inria (2018), https://ocaml

    Leroy, X., Doligez, D., Frisch, A., Garrigue, J., Rémy, D., Vouillon, J.: The OCaml System: Documentation and User’s Manual. Inria (2018), https://ocaml. org/manual/

    work page 2018

  25. [25]

    In: David, C., Sun, M

    Lidström, C., Gurov, D.: Contract based embedded software design. In: David, C., Sun, M. (eds.) Theoretical Aspects of Software Engineering. pp. 77–94. Springer Nature Switzerland, Cham (2023). https://doi.org/10.1007/978-3-031-35257-7_5

    work page doi:10.1007/978-3-031-35257-7_5 2023

  26. [26]

    Lin, F., Kim, D.J., Li, Z., Yang, J., Tse-Hsun, Chen: RobuNFR: Evaluating the robustness of large language models on non-functional requirements aware code generation (2025), https://arxiv.org/abs/2503.22851

    work page arXiv 2025

  27. [27]

    In: Di Giusto, C., Ravara, A

    Lopez Pombo, C.G., Melgratti, H., Martinez-Suñé, A.E., Anabia, D.S., Tuosto, E.: Behavioural, functional, and non-functional contracts for dynamic selection of services. In: Di Giusto, C., Ravara, A. (eds.) Coordination Models and Languages. pp. 153–174. Springer Nature Switzerland, Cham (2025). https://doi.org/10.1007/ 978-3-031-95589-1_8

    work page 2025

  28. [28]

    Loques, O., Sztajnberg, A., Curty, R., Ansaloni, S.: A contract-based approach to describe and deploy non-functional adaptations in software architectures. J. Braz. Comput. Soc.10(1), 5–18 (2004). https://doi.org/10.1007/BF03192350

    work page doi:10.1007/bf03192350 2004

  29. [29]

    Marjamäki, D., contributors: Cppcheck: A tool for static C/C++ code analysis (2026), https://cppcheck.sourceforge.io/

    work page 2026

  30. [30]

    MIRA Ltd: MISRA-C:2004 Guidelines for the use of the C language in critical systems. Tech. rep., Motor Industry Software Reliability Association (Oct 2004), https://misra.org.uk/misra-c

    work page 2004

  31. [31]

    Z3: An Efficient SMT Solver

    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–340. Springer Berlin Heidelberg, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    work page doi:10.1007/978-3-540-78800-3_24 2008

  32. [32]

    https://doi.org/10.48550/arXiv.2410.14835, arXiv:2410.14835

    Mukherjee, P., Delaware, B.: Towards Automated Verification of LLM- Synthesized C Programs (Oct 2024). https://doi.org/10.48550/arXiv.2410.14835, arXiv:2410.14835

    work page doi:10.48550/arxiv.2410.14835 2024

  33. [33]

    In: Proceedings of the ITT Workshop on Reusability in Programming

    Parnas, D.L., Clements, P.C., Weiss, D.M.: Enhancing reusability with information hiding. In: Proceedings of the ITT Workshop on Reusability in Programming. pp. 7–9 (1983). https://doi.org/10.1145/73103.73109

    work page doi:10.1145/73103.73109 1983

  34. [34]

    In: Steffen, B

    Patil, M.S., Ung, G., Nyberg, M.: Towards Specification-Driven LLM-Based Gen- eration of Embedded Automotive Software. In: Steffen, B. (ed.) Bridging the Gap Between AI and Reality - Second International Conference, AISoLA 2024, Crete, Greece, October 30 - November 3, 2024, Proceedings. Lecture Notes in Com- puter Science, vol. 15217, pp. 125–144. Springe...

    work page 2024

  35. [35]

    In: Tools and Algorithms for the 24 J

    Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., Le Gall, P.: MetAcsl: Speci- fication and verification of high-level properties. In: Tools and Algorithms for the 24 J. Amilon et al. Construction and Analysis of Systems. pp. 358–364. Springer International Pub- lishing, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_22

    work page doi:10.1007/978-3-030-17462-0_22 2019

  36. [36]

    Sevenhuijsen, M., Etemadi, K., Nyberg, M.: VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models (2024), https://arxiv.org/ abs/2411.19275

    work page arXiv 2024

  37. [37]

    Sevenhuijsen, M., Patil, M.S., Nyberg, M., Ung, G.: Generating safety-critical automotive C-programs using LLMs with formal verification. In: H. Gilpin, L., Giunchiglia,E.,Hitzler,P.,vanKrieken,E.(eds.)InternationalConferenceonNeu- rosymbolic Learning and Reasoning. Proceedings of Machine Learning Research, vol. 284, pp. 353–378. PMLR (08–10 Sep 2025), ht...

    work page 2025

  38. [38]

    In: 2024 2nd In- ternational Conference on Foundation and Large Language Models (FLLM)

    Slama, F., Lemire, D.: Comparative Analysis of Loop-Free Function Evaluation Using ChatGPT and Copilot with C Bounded Model Checking. In: 2024 2nd In- ternational Conference on Foundation and Large Language Models (FLLM). pp. 58–65 (2024). https://doi.org/10.1109/FLLM63129.2024.10852461

    work page doi:10.1109/fllm63129.2024.10852461 2024

  39. [39]

    Software & Systems Modeling14, 83–100 (2015)

    Soleimanifard, S., Gurov, D., Huisman, M.: Procedure-modular specification and verification of temporal safety properties. Software & Systems Modeling14, 83–100 (2015). https://doi.org/10.1007/s10270-013-0321-0

    work page doi:10.1007/s10270-013-0321-0 2015

  40. [40]

    Free Software Foundation (2026), https://gcc.gnu.org/onlinedocs/gcc/, GCC Ver- sion 16.0.1

    Stallman, R.M., Community, G.D.: Using the GNU Compiler Collection (GCC). Free Software Foundation (2026), https://gcc.gnu.org/onlinedocs/gcc/, GCC Ver- sion 16.0.1

    work page 2026

  41. [41]

    Stouls, N.: Aorai plug-in tutorial, https://frama-c.com/download/aorai/ aorai-manual.pdf

    work page

  42. [42]

    Sun, X., Ståhl, D., Sandahl, K., Kessler, C.: Quality assurance of LLM-generated code: Addressing non-functional quality characteristics (2025), https://arxiv.org/ abs/2511.10271

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  43. [43]

    In: International Requirements Engineering Conference

    Ung, G., Amilon, J., Gurov, D., Lidström, C., Nyberg, M., Palmskog, K.: Post-hoc formal verification of automotive software with informal requirements: An experi- ence report. In: International Requirements Engineering Conference. pp. 287–298 (2024). https://doi.org/10.1109/RE59067.2024.00035

    work page doi:10.1109/re59067.2024.00035 2024