{"id":"0718b652-db36-480d-9a3a-ad2b6574f610","arxiv_id":"2501.10889","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"AutoDeduct automatically infers missing formal annotations for helper functions in C programs and verifies the entry-point contract with Frama-C's WP plugin.","lead":"This paper introduces AutoDeduct, a tool that reads a C program with one hand-written specification and automatically writes the additional specifications required to formally verify the whole program. The authors test it on a simplified automotive software module and report successful verification in about 23 seconds.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Evaluation is a single hand-simplified 123 LOC module; without evidence that the simplification preserves the 5 Scania requirements, the claim that AutoDeduct verifies industrial C code is not supported.","rationale":"The paper is honest and the artifact is a real contribution. The functional inference via TriCera plus auxiliary inference via Eva, followed by WP verification, is a plausible pipeline, and the running example demonstrates the mechanism. The use of WP as the verification backend means that, for the simplified module, a successful run is real evidence that the toolchain works on that module. However, the conclusion in Section 5 generalizes from one simplified example to industrial C code. The reader's weakest assumption identifies exactly this gap: the simplification's behavior preservation is asserted, not demonstrated. I agree with that assessment. A secondary concern is the \"first to offer such a high degree of automation\" claim in Section 5, which is not backed by a comparison; but novelty claims are less load-bearing than the transferability of the evaluation. The internal consistency of the tool description is not in question. Therefore the verdict should remain conditional: the technical claims are plausible and worth accepting if the artifact runs, but the industrial conclusion needs either a behavior-preservation argument or additional case studies.","tokens_in":6546,"tokens_out":4116,"duration_ms":50919,"concrete_test":"Obtain the original 1400 LOC Scania module (previously used in [14]); instrument both it and the artifact's simplified 123 LOC module to log all outputs and assigned memory locations relevant to the 5 requirements, then run both on a test suite covering requirement boundaries (e.g., 0, 10, 11, and negative inputs for the saturate-like behavior). If the simplified module's observable behavior matches the original on all tests, the simplification concern is mitigated; any mismatch shows the verified contract does not transfer to the industrial module.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim in Section 5 is that AutoDeduct can \"automatically verify industrial C code specified with industrial requirements.\" The only support is Section 4: a 123 LOC simplified version of a 1400 LOC Scania module, with 5 selected requirements. The paper states that unsupported constructs were removed and \"certain pointer constructs\" were rewritten, but it gives no argument that these changes preserve the behaviors on which the 5 requirements depend. Pointer arithmetic and floating point are named unsupported (Section 3, Limitations); if any of the 5 requirements involves such constructs, then the verified contract is not the original requirement at all. The simplification also selects requirements (\"5 of its requirements\"), so the evaluation is cherry-picked with respect to tool capabilities. The technical contribution—inferring contracts for helper functions and verifying with WP—may be sound, but the load-bearing bridge from simplified example to industrial conclusion is absent. This is not a matter of consensus; it is missing evidence internal to the evaluation design.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":6830,"tokens_out":6590,"duration_ms":74492,"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":[{"comment":"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.","section":"Section 4 (Evaluation) and Section 5 (Conclusion)"},{"comment":"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.","section":"Section 5 (Conclusion)"},{"comment":"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.","section":"Section 3 (Running the toolchain)"}],"minor_comments":[{"comment":"The abstract contains a typo: \"AutoDecuct\" should be \"AutoDeduct.\"","section":"Abstract"},{"comment":"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.","section":"Section 3, Figure 3"},{"comment":"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.","section":"Section 4 (Evaluation)"},{"comment":"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.","section":"Section 4 (Evaluation)"},{"comment":"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.","section":"Section 3 (Limitations)"}],"recommendation":"major_revision","confidential_remarks":"For the editor: this is a short tool paper whose central technical approach appears sound, but the published claims overreach the evidence. The most important fix is to either add a requirement-preservation argument for the simplified Scania module or to explicitly limit the conclusion to the simplified module. The paper would also benefit from a more cautious wording of the \"first\" claim. These are fixable within the manuscript's scope, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: AutoDeduct is a real prototype that combines two previously separate Frama-C plugins—functional contract inference via TriCera and auxiliary annotation inference via Eva—into one toolchain, ships as a Docker image, and verifies a simplified Scania module in about 23 seconds. That is a genuine, reproducible contribution. The soft spot is exactly where the stress-test note points: the only evaluation is a 123-LOC simplified version of a 1400-LOC module, with five selected requirements, and the paper gives no argument that the simplifications preserve the behaviors on which those requirements depend. The conclusion that AutoDeduct 'can automatically verify industrial C code' is not supported by the evidence.\n\nWhat is actually new: the integration, the first public prototype, and the annotated artifact. The technical description is clear, and the limitations section is honest—it names unsupported C features up front, including pointer arithmetic and floating point. If any of the five Scania requirements touches those constructs, the simplified module may not even exercise the relevant behavior. The core workflow—entry-point contract plus source, infer helper contracts, verify with WP—is not circular, since the goal contract is external, and the inferred contracts are property-guided and context-specific, as the paper notes.\n\nWhere it falls short: one simplified case study, no baseline comparison, and a 'first' claim that would need a broader survey to back. The cherry-picking of requirements is a real concern, but it is a concern about the strength of the evaluation, not about the tool's existence. If the artifact runs as described, the technical contribution is solid.\n\nWho this is for: researchers working on contract inference and deductive verification for C, and toolchain builders in the formal-verification space. They will get value from the architecture and the honest limitations. It deserves a serious referee: the artifact is available, the method is described well enough to reproduce, and the integration is a legitimate step forward. The referee should push for either a broader evaluation or a more modest conclusion.","headline":"Solid prototype paper with a reproducible artifact, but the industrial verification claim outruns the single simplified case study.","tokens_in":7237,"tokens_out":2563,"would_cite":true,"duration_ms":25710,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"AutoDeduct writes every missing C contract and verifies the module from a single entry-point spec.","keywords":["deductive verification","contract inference","ACSL","C programs","automated annotation","Horn clauses","abstract interpretation","industrial case study"],"falsifier":"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.","tokens_in":6356,"feed_emoji":"✅","tokens_out":5949,"duration_ms":55344,"temperature":0.7,"pith_summary":"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.","feed_headline":"AutoDeduct supplies every missing C contract and verifies the module","feed_subtitle":"Given one entry-point contract it annotates every helper function and proves five industrial requirements in about 23 seconds.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the functional-contract inference plugin that extracts ACSL requires and ensures clauses from Horn-clause solutions.","marker":"[3]"},{"why":"Introduces the constraint-based contract inference method that the functional plugin builds on.","marker":"[2]"},{"why":"Previous work on synthesizing auxiliary annotations that the auxiliary plugin extends.","marker":"[12]"},{"why":"Earlier auxiliary-annotation synthesis effort that the auxiliary plugin builds on.","marker":"[18]"},{"why":"Thesis that defines the functional-versus-auxiliary annotation classification used throughout the paper.","marker":"[11]"},{"why":"Defines the host platform that integrates the inference plugins and the verification engines.","marker":"[7]"},{"why":"Documents the weakest-precondition verification engine that checks the final annotated program.","marker":"[5]"},{"why":"Documents the abstract-interpretation value analysis used to generate ranges, pointer validity, and assigns clauses.","marker":"[6]"},{"why":"Reports the earlier manual two-person-month verification of the industrial module, the baseline for the case study.","marker":"[14]"}],"fun_headline_variants":["AutoDeduct infers every C contract from one entry-point spec","Two-pass contract inference turns one spec into full C verification","AutoDeduct annotates all helpers, proves five requirements in 23s","One entry-point contract is all AutoDeduct needs to verify C code","AutoDeduct's two-pass inference makes C verification hands-free"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["AutoDeduct infers every C contract from one entry-point spec","Two-pass contract inference turns one spec into full C verification","AutoDeduct annotates all helpers, proves five requirements in 23s","One entry-point contract is all AutoDeduct needs to verify C code","AutoDeduct's two-pass inference makes C verification hands-free"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000801,"raw_usage":{"total_tokens":3483,"prompt_tokens":871,"completion_tokens":2612,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":487,"completion_tokens_details":{"reasoning_tokens":2521}},"tokens_in":487,"tokens_out":2612,"duration_ms":18541,"temperature":1.0,"reasoning_tokens":2521,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T18:51:28.980332+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":": An Exercise in Mind Reading: Automatic Contract Inference for Frama- C, pp","cited_arxiv_id":null,"evidence_quote":"Supplies the functional-contract inference plugin that extracts ACSL requires and ensures clauses from Horn-clause solutions."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces the constraint-based contract inference method that the functional plugin builds on."},{"cited_title":"Master’s thesis, KTH Royal Institute of Technology (2021)","cited_arxiv_id":null,"evidence_quote":"Previous work on synthesizing auxiliary annotations that the auxiliary plugin extends."},{"cited_title":"Master’s thesis, KTH Royal Institute of Techn ology (2021)","cited_arxiv_id":null,"evidence_quote":"Earlier auxiliary-annotation synthesis effort that the auxiliary plugin builds on."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Thesis that defines the functional-versus-auxiliary annotation classification used throughout the paper."},{"cited_title":"CEA LIST, Inria, http://frama-c.com/download/frama-c-user-manual.pdf 7","cited_arxiv_id":null,"evidence_quote":"Defines the host platform that integrates the inference plugins and the verification engines."},{"cited_title":"CEA LIST (2024), https://frama-c.com/download/frama-c-wp-manual.pdf","cited_arxiv_id":null,"evidence_quote":"Documents the weakest-precondition verification engine that checks the final annotated program."},{"cited_title":"CEA LIST (2024), http://frama-c.com/download/frama-c-eva-manual.pdf","cited_arxiv_id":null,"evidence_quote":"Documents the abstract-interpretation value analysis used to generate ranges, pointer validity, and assigns clauses."},{"cited_title":"In: Lever- aging Applications of Formal Methods, Verification and Vali dation","cited_arxiv_id":null,"evidence_quote":"Reports the earlier manual two-person-month verification of the industrial module, the baseline for the case study."}],"review_version":1}