Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

AutoDeduct: A Tool for Automated Deductive Verification of C Code

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

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

Pith's one-line read AutoDeduct writes every missing C contract and verifies the module from a single entry-point spec.

desk verdict Solid prototype paper with a reproducible artifact, but the industrial verification claim outruns the single simplified case study. read the letter →

arxiv 2501.10889 v1 pith:ONXHFMQ5 submitted 2025-01-18 cs.LO cs.SE

Jesper Amilon , Dilian Gurov , Christian Lidström , Mattias Nyberg , Gustav Ung , Ola Wingbrant This is my paper · ORCID
classification cs.LOcs.SE
keywords deductiveverificationcontractinferenceACSLCprogramsautomatedannotationHornclausesabstractinterpretationindustrialcasestudy
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

Deductive verification of C code normally requires a human to annotate every helper function with a formal contract, a burden measured in person-months on industrial code. AutoDeduct aims to remove that bottleneck: given a C module whose entry-point function already has an ACSL contract, it automatically infers contracts for all helper functions and then proves the annotated program with a weakest-precondition verifier. The paper presents the first public prototype of this toolchain and reports that on a 123-line simplification of a 1400-line automotive module, it infers all contracts and discharges the verification in about 23 seconds. The point of the paper is that this combination of inference techniques makes deductive verification practical for modules whose requirements are specified at the entry-point level.

What carries the argument

The load-bearing mechanism is the pairing of two complementary contract-inference plugins inside the host verification platform, one for functional annotations and one for auxiliary annotations. Functional inference works by translating the program and the entry-point contract into a set of Horn clauses, where each helper function is associated with an unknown pre-condition and post-condition predicate; a solver for these constraints yields sufficient conditions from which ACSL requires and ensures clauses are extracted. Auxiliary inference runs the platform's abstract-interpretation value analysis to synthesize the extra annotations, such as variable ranges, pointer validity, and assigns clauses, that the proof needs but that do not describe the function's primary behavior. The verification engine then proves every contract, so the trust base is only the final proof step, not the inference heuristics.

What would settle it

Run AutoDeduct on the original, unmodified 1400-line module with the same five requirements; if verification fails or requires rewriting a construct that the simplification removed, the reported success does not transfer to the real module.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that property-guided contract inference can be staged in two complementary passes: a functional pass that encodes the program as Horn clauses and solves for pre-condition and post-condition predicates for each called function, and an auxiliary pass that uses abstract interpretation to generate range, pointer-validity, and assigns annotations. Together the passes produce a fully annotated file whose helper contracts are strong enough for the existing weakest-precondition engine to verify the entry-point contract. The inferred contracts are intentionally context-specific: they may require, for example, that a parameter equal a constant imposed by the single call site, so they are sufficient for the current program rather than general API specifications. On the industrial case study the toolchain verifies the five stated requirements and emits the annotated module as an artifact.

Load-bearing premise

The paper's industrial claim rests on the 123-line simplified module preserving every behavior of the original 1400-line module that the five selected requirements depend on.

Editorial extensions

If this is right

  • A verification engineer only writes the entry-point contract; helper-function annotations are produced automatically, so per-module annotation effort drops from person-months to the time the toolchain runs.
  • Because inferred contracts are context-specific, the same helper called from different entry points may get different inferred contracts, which keeps the generated proof obligations small.
  • The toolchain outputs the fully annotated C file, so the result is an auditable artifact, not just a yes-or-no verdict.
  • Automating auxiliary annotations such as pointer validity and assigns clauses removes a large fraction of the manual proof burden for embedded C code.
  • Automated inference makes the deductive verification workflow usable at industrial scale for modules whose requirements are stated at module level.

Reading between the lines

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

  • If the simplification step in the case study is faithful, the same staged inference should transfer to other embedded modules with entry-point contracts, but the tool's current exclusion of pointer arithmetic, nested pointers, local statics, and floating point bounds the class of programs it can absorb without rewriting.
  • The context-specific nature of inferred contracts suggests a module-level verification style: rather than aiming for reusable library contracts, AutoDeduct treats each call tree as a proof object, which may make it easier to integrate into existing OEM requirement workflows.
  • One testable extension would be to generate a diff report between the simplified and original module, mapping each removed construct to the requirements it could affect, so that preservation of behavior is argued mechanically rather than by hand.
  • Because loop invariants are not yet inferred, the toolchain currently targets modules whose helper functions avoid unbounded loops; adding invariant inference would remove the last major structural restriction.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper presents AutoDeduct, a Frama-C-based toolchain that, given a C module whose entry-point function is equipped with an ACSL contract, automatically infers contracts for helper functions and then verifies the annotated module with WP. Functional contract inference is performed via a TriCera-backed plugin, while auxiliary annotations (ranges, pointer validity, assigns clauses) are derived with an Eva-backed plugin. The tool is evaluated on a 123-LOC simplified version of a 1400-LOC Scania module, with 5 of its requirements encoded as ensures clauses in the entry-point contract; the paper reports that verification succeeds in roughly 23 seconds. The abstract and conclusion claim that this demonstrates automatic deductive verification of industrial C code.

Significance. If the reported behavior is reproducible, AutoDeduct is a useful step toward reducing the manual annotation burden of deductive verification. The paper is transparent about the architecture, clearly separates functional from auxiliary contract inference, makes the prototype available as a Docker image and artifact, and reports concrete timings. A notable strength is that the final WP verification checks the inferred helper contracts against their own bodies, so the successful verification is not circular: the entry-point contract is verified using helper contracts that are themselves proved. The significance is that of a promising prototype evaluated on one adapted industrial example, rather than a demonstrated, general industrial solution; the main gap is the missing argument that the simplified module preserves the behaviors needed for the claimed industrial requirements.

major comments (3)
  1. [Section 4 (Evaluation) and Section 5 (Conclusion)] The evaluation does not establish that the 123-LOC simplified module preserves the behaviors needed for the five Scania requirements. The manuscript says that parts "not relevant for the specified requirements" were removed and "certain pointer constructs" were rewritten, but it provides no requirement-by-requirement mapping to the simplified code and no argument that the transformations preserve the relevant program states. This matters because Section 3 lists floating-point arithmetic, pointer arithmetic, nested pointers, and local static variables as unsupported features; if any of the five requirements depends on such constructs, the contract verified by AutoDeduct is not the original industrial requirement. As written, the verification success supports the claim that AutoDeduct can verify the simplified module, but not the Section 5 claim that it can "automatically verify industrial C code specified with industrial requirements." Please either add a preservation/traceability argument (in the paper or in a documented artifact) or restrict the conclusion to the simplified module.
  2. [Section 5 (Conclusion)] The sentence "We believe our toolchain to be the first one to offer such a high degree of automation" is an unsupported "first" claim. Section 4 only states that the authors are not aware of comparable toolchains; no systematic comparison or literature search is reported. This should be softened to "to the best of our knowledge" or supported by a concrete comparison with existing contract-inference tools, including those cited in Section 1.
  3. [Section 3 (Running the toolchain)] The paper claims that the verification trust base "does not extend beyond the mature WP plugin of Frama-C." While this is true if WP verifies every inferred helper contract, the practical usefulness of the toolchain still depends on the termination and precision of the TriCera and Eva backends: if those components produce too-weak contracts, WP will fail on the entry-point proof. The paper should state that inference failure can block verification and that the current prototype provides no automated way to repair weak inferred contracts. This is a limitation that should be acknowledged explicitly rather than left implicit.
minor comments (5)
  1. [Abstract] The abstract contains a typo: "AutoDecuct" should be "AutoDeduct."
  2. [Section 3, Figure 3] The text says "The inferred contracts for saturate and read_input are shown in Figure 3," but Figure 3 displays contracts for saturate and write_output; the text and figure caption should be made consistent.
  3. [Section 4 (Evaluation)] The phrase "5 of its requirements" should be accompanied by a statement of the selection criteria; specifying whether the requirements were chosen before or after assessing tool support would mitigate the impression of cherry-picking with respect to the supported C subset.
  4. [Section 4 (Evaluation)] The paper does not report the versions of Frama-C, WP, Eva, and TriCera, nor the machine on which the 23-second run was measured; adding version numbers and a short command transcript would improve reproducibility.
  5. [Section 3 (Limitations)] Since loop-invariant inference is listed as not yet implemented, the future-work paragraph in Section 5 should mention loop invariants explicitly; otherwise readers may assume the toolchain can handle arbitrary loops in the simplified module without an additional annotation burden.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: inferred helper contracts are checked by WP and are not used to define the entry-point goal.

full rationale

The derivation chain is not circular. AutoDeduct takes as input a C program and an externally provided ACSL contract for the entry point; the functional and auxiliary inference plugins generate candidate contracts for helper functions using TriCera and Eva, and the final WP run verifies both the entry-point contract and the inferred helper contracts. The paper states: "The verification with WP ensures that the entry-point function satisfies the provided contract, and that every helper function satisfies its inferred contract." Thus the goal (the entry-point contract) is not defined in terms of the inferred helper contracts; rather, the inferred contracts are synthesized from the program and the goal and then independently checked by WP. Since WP must prove the helper contracts against the code, the verified result does not reduce to the inference's own output, even if the inference were unsound. The authors' citations to their own prior work describe components and earlier case studies, but the central toolchain claim—that the entry-point contract is eventually proved by WP—does not depend on those citations for the truth of the result. The acknowledged limitations on floating-point, pointers, and loop invariants, together with the evaluation on a simplified 123-LOC module with 5 selected requirements, are threats to the strength of the industrial conclusion, but they are matters of evaluation scope and external validity, not circular reasoning. No step in the paper exhibits an equation-by-construction reduction or a fitted parameter renamed as a prediction.

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

No numeric free parameters are fitted in this paper. The central claims inherit trust from external tools (WP, TriCera, Eva) and from the equivalence of the simplified evaluation module to the industrial module; both are assumptions rather than results established here.

assumptions (5)
  • domain assumption Frama-C WP plugin is sound: successful WP verification implies the annotated C functions satisfy their ACSL contracts.
    Used as the verification backend; soundness of the tool's claim inherits from WP soundness (Section 3, architecture).
  • domain assumption TriCera's Horn clause encoding is sound and produces sufficient pre/post conditions for the C semantics.
    Functional inference relies on the TriCera backend (Section 3, Functional contract inference); no soundness proof is given in this paper.
  • domain assumption Eva abstract interpretation over-approximates reachable states, so derived ranges, pointer validity, and assigns clauses are accurate.
    Auxiliary inference uses Eva (Section 3, Auxiliary contract inference).
  • domain assumption The simplified 123 LOC module faithfully preserves behaviors relevant to the 5 requirements of the original 1400 LOC industrial module.
    Section 4 says unsupported constructs were removed and requirements were selected; the transfer of the evaluation to the industrial module depends on this.
  • domain assumption The provided entry-point contract is the intended specification and is itself correct.
    The tool assumes an entry-point contract as input (Section 3); if this contract is wrong, the verification result is not meaningful.

how reviews work

0 comments
Cite this review

Pith. "Pith review of AutoDeduct: A Tool for Automated Deductive Verification of C Code." pith.science (2026). https://pith.science/paper/ONXHFMQ5

@misc{pith2026250110889,
  author       = {Pith},
  title        = {Pith review of: AutoDeduct: A Tool for Automated Deductive Verification of C Code},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ONXHFMQ5}},
  note         = {Machine review of arXiv:2501.10889}
}
read the original abstract

Deductive verification has become a mature paradigm for the verification of industrial software. Applying deductive verification, however, requires that every function in the code base is annotated with a function contract specifying its behaviour. This introduces a large overhead of manual work. To address this challenge, we introduce the AutoDeduct toolchain, built on top of the Frama-C framework. It implements a combination of techniques to automatically infer contracts for functions in C programs, in the syntax of ACSL, the specification language of Frama-C. Contract inference in AutoDecuct is implemented as two plugins for Frama-C, each inferring different types of annotations. We assume that programs have an entry-point function already equipped with a contract, which is used in conjunction with the program source code to infer contracts for the helper functions, so that the entry-point contract can be verified. The current release of AutoDeduct is the first public prototype, which we evaluate on an example adapted from industrial software.

Figures

Figures reproduced from arXiv: 2501.10889 by the authors.

Figure 1
Figure 1. Example program with a main function and three help [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Architecture of AutoDeduct meaning that it infers contracts that are strong enough for verifying the current program, but they may not generalise to other contexts. We classify annotations within ACSL contracts as either functional or aux￾iliary [11]. The functional annotations directly concern the behaviour of the function, typically by relating input values to output values of program vari￾ables. Auxiliary annotat… view at source ↗
Figure 3
Figure 3. Inferred contracts for the program write_output and saturate the program as a set of Horn clauses, where each called function is associated with a pair of predicates representing the pre-condition and post-condition. An interpretation for these predicates represents sufficient conditions for the pro￾gram to be correct. Based on this solution, contracts for the helper functions can be extracted. For further technical… view at source ↗

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. Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification

    cs.SE 2026-07 conditional novelty 7.0 of 10

    Caller-sufficient partial contracts, LLM-inferred and verifier-enforced, soundly prove safety-preserving regression equivalence without full behavioral specs.

Reference graph

Works this paper leans on

19 extracted references · 13 canonical work pages · cited by 1 Pith paper

  1. [1]

    In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGA CT Symposium on Principles of Programming Languages, POPL 201 6, St

    Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal spe cification syn- thesis. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGA CT Symposium on Principles of Programming Languages, POPL 201 6, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 789–801 (2016 ). https://doi.org/10.1145/2837614.2837628

    arXiv 2016

  2. [2]

    Alshnakat, A., Gurov, D., Lidström, C., Rümmer, P.: Cons traint-Based Contract Inference for Deductive Verification, pp. 149–176 . Springer In- ternational Publishing, Cham (2020). https://doi.org/10 .1007/978-3-030- 64354-6_6

    work page 2020

  3. [3]

    : An Exercise in Mind Reading: Automatic Contract Inference for Frama- C, pp

    Amilon, J., Esen, Z., Gurov, D., Lidström, C., Rümmer, P. : An Exercise in Mind Reading: Automatic Contract Inference for Frama- C, pp. 553–582. Springer International Publishing, Cham (2 024). https://doi.org/https://doi.org/10.1007/978-3-031-55608-1_13

    work page doi:10.1007/978-3-031-55608-1_13

  4. [4]

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

    work page 2024

  5. [5]

    CEA LIST (2024), https://frama-c.com/download/frama-c-wp-manual.pdf

    Baudin, P., Bobot, F., Correnson, L., Dargaye, Z., Blan- chard, A.: WP Plug-in Manual. CEA LIST (2024), https://frama-c.com/download/frama-c-wp-manual.pdf

    work page 2024

  6. [6]

    CEA LIST (2024), http://frama-c.com/download/frama-c-eva-manual.pdf

    Bühler, D., Cuoq, P., Yakobowski, B.: Eva - The Evolved Value Analysis plug-in. CEA LIST (2024), http://frama-c.com/download/frama-c-eva-manual.pdf

    work page 2024

  7. [7]

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

    Correnson, L., Cuoq, P., Kirchner, F., Maroneze, A., Pre vosto, V., Puc- cetti, A., Signoles, J., Yakobowski, B.: Frama-C User Manua l. CEA LIST, Inria, http://frama-c.com/download/frama-c-user-manual.pdf 7

    work page

  8. [8]

    Dijkstra, E.W.: Guarded commands, nondeterminacy and f ormal derivation of programs. Commun. ACM 18(8), 453–457 (Aug 1975). https://doi.org/10.1145/360933.360975

    arXiv 1975

Show all 19 references
  1. [9]

    In: Refle ctions on the Work of C

    Gordon, M., Collavizza, H.: Forward with Hoare. In: Refle ctions on the Work of C. A. R. Hoare., pp. 101–121. Springer (2010). https://doi.org/10.1007/978-1-84882-912-1_5

    2010 doi

  2. [10]

    , Yakobowski, B.: Frama-C: A Software Analysis Perspective

    Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J. , Yakobowski, B.: Frama-C: A Software Analysis Perspective. Formal Aspects o f Computing (2015). https://doi.org/10.1007/978-3-642-33826-7_16

    2015 doi

  3. [11]

    Lidström, C.: Automated Deductive Verification of Safe ty-Critical Em- bedded Software. Ph.D. thesis, KTH, Theoretical Computer S cience, TCS (2024), qC 20240223

    2024

  4. [12]

    Master’s thesis, KTH Royal Institute of Technology (2021)

    Manjikian, H.: Improving the Synthesis of Annotations for Partially Au- tomated Deductive Verification. Master’s thesis, KTH Royal Institute of Technology (2021)

    2021

  5. [13]

    In: Ver- ification, Model Checking, and Abstract Interpretation, 9t h International Conference, VMCAI 2008, San Francisco, USA, January 7-9, 20 08, Pro- ceedings

    Moy, Y.: Sufficient preconditions for modular assertion checking. In: Ver- ification, Model Checking, and Abstract Interpretation, 9t h International Conference, VMCAI 2008, San Francisco, USA, January 7-9, 20 08, Pro- ceedings. pp. 188–202 (2008). https://doi.org/10.1007/9 78-3-...

    2008 doi

  6. [14]

    In: Lever- aging Applications of Formal Methods, Verification and Vali dation

    Nyberg, M., Gurov, D., Lidström, C., Rasmusson, A., Wes tman, J.: Formal verification in automotive industry: Enablers and obstacle s. In: Lever- aging Applications of Formal Methods, Verification and Vali dation. In- dustrial Practice: 8th International Symposium, ISoLA 201 8, ...

    2018 doi

  7. [15]

    Seghir, M.N., Kroening, D.: Counterexample-guided pr econdition in- ference. In: Programming Languages and Systems - 22nd Europ ean Symposium on Programming, ESOP 2013, Held as Part of the Euro - pean Joint Conferences on Theory and Practice of Software, E TAPS 2013, Rome, Ita...

    2013 doi

  8. [16]

    In: Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Pr oceedings

    Seghir, M.N., Schrammel, P.: Necessary and sufficient pr econditions via eager abstraction. In: Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Pr oceedings. pp. 236–254 (2014). https://doi.org/10.1007/978-3-319- 12736-1_13

    2014 doi

  9. [17]

    CoRR abs/1905.06847 (2019), http://arxiv.org/abs/1905.06847 8

    Singleton, J.L., Leavens, G.T., Rajan, H., Cok, D.R.: I nfer- ring concise specifications of APIs. CoRR abs/1905.06847 (2019), http://arxiv.org/abs/1905.06847 8

    2019 arXiv

  10. [18]

    Master’s thesis, KTH Royal Institute of Techn ology (2021)

    Skantz, D.: Synthesis of Annotations for Partially Aut omated Deductive Verification. Master’s thesis, KTH Royal Institute of Techn ology (2021)

    2021

  11. [19]

    , Palm- skog, K.: Post-hoc formal verification of automotive softwa re with in- formal requirements: An experience report

    Ung, G., Amilon, J., Gurov, D., Lidström, C., Nyberg, M. , Palm- skog, K.: Post-hoc formal verification of automotive softwa re with in- formal requirements: An experience report. In: 2024 IEEE 32 nd Inter- national Requirements Engineering Conference (RE). pp. 28 7–298 (2024)....

    2024

Pith tools

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