{"id":"8df15598-4400-4295-a986-4a9fe5ddbd60","arxiv_id":"2501.16310","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A standalone program-transformation framework lets off-the-shelf reachability verifiers handle termination, no-overflow, and memory cleanup by rewriting the input C program.","lead":"The authors build TransVer, a framework that rewrites C programs so that properties like termination, no-overflow, and memory cleanup become simple reachability checks. This lets ordinary reachability verifiers handle more complex specifications as a black-box preprocessing step.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The central equivalence claim is not proven and is known to fail for the termination transformation on dynamic structures; the benchmark subset excludes exactly those cases, so the \"extends verifiers\" conclusion is only supported for a restricted program class.","rationale":"The reader's weakest assumption is exactly the one I would press: the transformations' correctness is asserted rather than proved, and the authors voluntarily disclose a real unsoundness for dynamic structures in the termination transformation. I agree with the CONDITIONAL verdict. This is not a rejection: the paper is a serious engineering contribution with a plausible modular architecture, a careful evaluation using BenchExec and established verifiers, and honest reporting of limitations, including the 17 removed tasks with undefined behavior and the Table 5 false verdict caused by incomplete function-pointer handling. The central claim is nevertheless stated more broadly than the evidence supports. The benchmark subset removes structures and arrays precisely where the termination transformation is known to be unsound, so the empirical results cannot license an unqualified 'extend existing verifiers to be effective' conclusion. A curated differential suite over dynamic structures would settle whether the unsoundness is practically observable, and a correctness proof for the finite-state subset would define exactly what the framework guarantees. Neither check would overturn conditional acceptance, but either would sharpen the claim and reduce the residual risk. For these reasons, the reader's CONDITIONAL verdict remains appropriate, and no adjustment is needed.","tokens_in":20407,"tokens_out":4854,"duration_ms":54771,"concrete_test":"Construct or collect a curated suite of terminating C programs over dynamically allocated linked structures with known ground truth (e.g., list reversal, sorted insertion, and traversals with structural mutation), then run TransVer's termination transformation followed by a reachability verifier such as UAutomizer-R or CPAchecker-R. If any terminating program yields a non-termination alarm, the transformation is unsound on a class the paper claims to extend and the conclusions must be restricted; if none do over a sufficiently diverse suite, the unsoundness remains theoretical but the practical extension claim is strengthened. A complementary check would be to formalize the IA-to-CFA sequentialization semantics and prove that, for the declared finite-state subset, P |= termination iff P' |= reachability.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing step is the claimed equivalence P |= phi iff P' |= reachability for the composed transformations. Section 4 defines the sequentialization operator ⊗ and the instrumentation operator ⊎ operationally (Alg. 1, Eqs. 1-4), but no correctness theorem is stated or proved: there is no argument that every IA transition placed before or after a matched CFA edge preserves the semantics of the original operation sequence, nor that the wildcard pattern-matching is total for the supported subset. More concretely, the paper itself flags a failure: the termination IA in Fig. 6 is 'complete but not sound' for dynamic structures, because an infinite execution over a linked list can avoid ever revisiting a full state. The evaluation then removes tasks containing structures and arrays from the termination and no-overflow subsets, and Table 5 records an incorrect memory-cleanup verdict caused by function-pointer handling. Thus the experimental evidence supports the 'extends existing verifiers' claim only for programs whose variables have finite ranges and that avoid the excluded constructs; for the general C programs the framework advertises, the central equivalence can fail. Without either a proof covering the supported subset or a differential evaluation on the excluded and dynamic-structure classes, the strongest claim is under-supported rather than demonstrated.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a modular program-transformation framework, TransVer, that turns a C verification task P |= phi into a reachability task P' |= reachability by instrumenting the input program rather than a verifier's internal representation. Specifications are written as instrumentation automata (IA), and two operators, sequentialization (⊗) and instrumentation (⊎), are defined operationally in Section 4. The framework is instantiated for three SV-COMP specifications: no-overflow, termination, and memory cleanup; Section 6 sketches an explicit-liveness transformation. The evaluation compares reachability-only verifiers applied to transformed programs against native verifiers on SV-COMP 2024 benchmark subsets, and reports that the compositions are competitive in both effectiveness and efficiency.","tokens_in":20676,"tokens_out":5536,"duration_ms":59176,"significance":"If the central equivalence P |= phi iff P' |= reachability holds on the claimed input class, this is a practically useful contribution: it makes specification support a black-box preprocessing step, leverages mature reachability engines for other properties, and is backed by an open-source implementation and a broad experimental comparison over official SV-COMP tasks. The paper also credits prior work for the liveness-to-safety idea and carefully removes tasks with undefined behavior from the termination comparison. However, the correctness of the central operators is not demonstrated, and the paper itself records known limitations (termination on dynamic structures, one memory-cleanup verdict involving function pointers). The experimental claims therefore currently support the framework's usefulness only for the restricted, finite-state fragment of C that the paper actually evaluates.","major_comments":[{"comment":"The load-bearing claim of the paper is that composing the sequentialization operator ⊗ and the instrumentation operator ⊎ preserves the verification question: P |= phi iff P' |= reachability. No correctness theorem is stated or proved. Algorithm 1 and Eqs. (1)-(4) define the construction operationally, but there is no argument that (a) pattern matching is total on the supported subset, (b) an IA operation is inserted exactly once per matched CFA edge in the intended order, (c) unmatched edges are passed through without changing semantics, and (d) new locations introduced by NE do not affect program behavior. Since all research questions in Section 7 depend on this equivalence, the paper needs a formal theorem with a proof, or at minimum a precise statement of the supported input class together with a correctness argument for that class.","section":"Section 4, Algorithm 1 and Eqs. (1)-(4)"},{"comment":"The paper states that the termination transformation is 'complete but not sound' for dynamic structures such as linked lists, because an infinite execution can avoid revisiting the same full state. The evaluation then removes tasks containing structures and arrays from the termination and no-overflow subsets. This means the headline claim that the framework 'can extend existing verifiers to be effective on specifications that they do not support natively' is demonstrated only for programs whose variables range over finite domains, not for general C programs. The paper should either prove soundness for the exact supported subset and state that subset prominently, include the excluded program classes in the evaluation, or narrow the abstract and conclusion claims.","section":"Section 5, termination IA (Fig. 6) and Section 7 benchmark subset"},{"comment":"The memory-cleanup transformation is described as sound and complete because 'we handle all the relevant standard functions for memory allocation'. Table 5, however, reports one incorrect CPAchecker-R alarm, and the text attributes it to incomplete handling of function pointers. Function pointers are part of the C language and appear in the evaluated benchmark set, so the claimed soundness is overbroad as written. The paper should qualify the supported input class for memory cleanup, state what happens to function-pointer calls, and either exclude such tasks from the claim or handle them in the transformation.","section":"Section 5, memory cleanup IA (Fig. 7) and Table 5"},{"comment":"The threat-to-validity paragraph asserts that all incorrect results were inspected and none were caused by the transformation, but no procedure or evidence is given. Because incorrect verdicts appear in the results for the composed verifiers (e.g., 8 incorrect CPAchecker-R verdicts for no-overflow in Table 3), the reader cannot evaluate whether these lie inside the supported subset or whether they indicate a transformation bug. Please describe the inspection methodology, report the task categories of the incorrect verdicts, and make the transformed programs and inputs available so the claim is checkable.","section":"Section 7.5, Internal Validity"}],"minor_comments":[{"comment":"The text contains a typo: 'initeliaze_automata' should be 'initialize_automata'.","section":"Section 4, example"},{"comment":"The first data column mixes row labels with benchmark totals ('Correct 890', 'Proofs 615', 'Alarms 275'), which is confusing. Please reformat the table so the row labels are separated from the per-tool counts, and explicitly state that 615 and 275 are the ground-truth proof and alarm counts in the benchmark set.","section":"Table 3"},{"comment":"The soundness statement for no-overflow is conditional on decomposing complex arithmetic expressions and tracking signed-integer types, but the decomposition is not described. A short example of how a multi-operation line is split would make the supported input class clearer.","section":"Section 5, no-overflow IA"},{"comment":"The choice of the 'third-best tool' as a baseline is explained informally ('still competitive ... unlikely to contain bugs'). Please state the exact ranking criterion and why the third-best tool is more appropriate than the best or second-best tool for the comparison.","section":"Section 7.1"},{"comment":"The reference to 'Biere and Schuppan' should be checked against the bibliography entry [68], which lists Schuppan and Biere as authors.","section":"Section 6"}],"recommendation":"major_revision","confidential_remarks":"The core idea is attractive and the experimental setup is serious, but the missing correctness proof for ⊗ and ⊎ is a fundamental gap that cannot be patched by evaluation alone. The paper's own admission about the termination transformation on dynamic structures, combined with the benchmark removal of structures and arrays, makes the abstract's unqualified claim too strong. I would ask the authors to provide a formal correctness statement for a precisely delimited supported subset, or to substantially soften the claims and add a differential evaluation on the excluded classes."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: This is a solid, honest engineering paper. It packages three known specification-to-reachability transformations (termination via state repetition, no-overflow via assertion injection, memory cleanup via monitor automaton) as standalone C-to-C rewrites, so any reachability verifier can be pointed at these properties. The individual transformations are not new, and the framework is explicitly inspired by BLAST/SLIC, but the modular input-level packaging and the careful comparison against native-support tools are genuinely useful. The open-source TransVer implementation is a concrete asset.\n\nWhat the paper does well: the evaluation is systematic and uses the strongest available reachability verifiers (UAutomizer, UTaipan, CPV, Theta, EmergenTheta). For the supported task subsets, the transformed programs let reachability verifiers match or sometimes beat native tools. The finding that 17 termination tasks contained undefined signed-overflow behavior, which they reported back to the benchmark repository, is a nice side contribution. The RQ4 comparison of input-level vs internal transformation is informative and shows no systematic degradation.\n\nThe soft spots are real, and the paper mostly owns them. The central equivalence P |= phi iff P' |= reachability is stated but not proved for the sequentialization and instrumentation operators. Section 4 gives an operational description and an algorithm, but no correctness theorem. The paper explicitly notes the termination transformation is 'complete but not sound' for dynamic structures like linked lists, because an infinite run can avoid revisiting a full state. Then the termination and no-overflow benchmark subsets remove programs containing structures and arrays. So the headline claim—that the framework extends verifiers to specifications they do not natively support—is only demonstrated for programs with finite-range variables and without those constructs. That is a significant restriction for C programs. One incorrect memory-cleanup verdict due to function pointers is reported; they attribute it to incomplete handling in the transformation, which is the kind of thing a correctness proof would catch.\n\nNone of this kills the paper. The work is what it claims to be for the supported subset, and the limitations are stated rather than hidden. But for a strong publication I would want either a proof or a precise characterization of the supported subset plus a differential evaluation on the excluded classes.\n\nVerdict: send it to review. A serious referee will ask for the correctness argument and a clearer scope statement, but the engineering and evaluation deserve the attention.","headline":"A genuinely useful engineering paper that packages known specification-to-reachability transformations as input-level rewrites, with a strong but restricted evaluation; the unproved equivalence claim is the main weakness.","tokens_in":21154,"tokens_out":5568,"would_cite":false,"duration_ms":39873,"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":"The paper claims that composing an instrumentation-automaton-based program transformation with a reachability verifier preserves the specification, and makes off-the-shelf reachability verifiers effective on termination, no-overflow, and…","keywords":["software verification","program transformation","reachability","instrumentation automata","termination","no-overflow","memory cleanup","liveness"],"falsifier":"Run the termination transformation on a terminating program whose loop traverses a linked list created with malloc, so each iteration visits a fresh heap address; if the instrumented program passes the reachability check (reports no repeated state), then the transformation has wrongly certified termination. Equivalently, search the benchmark set for any program where a reachability verifier on the transformed program gives a different verdict than a trusted native verifier on the original program, and confirm the difference is caused by the transformation rather than verifier imprecision.","tokens_in":20240,"feed_emoji":"⚙️","tokens_out":5809,"duration_ms":49920,"temperature":0.7,"pith_summary":"This paper tries to establish that specification checking can be decoupled from verification algorithms: instead of teaching a verifier a new property, transform the input C program so the property becomes an ordinary reachability check, and reuse any existing reachability verifier unchanged. The authors build a framework around instrumentation automata, which specify how to insert monitoring code (ghost variables, assertions, state-saving) into a program, and implement three concrete instantiations: termination, no-overflow, and memory cleanup. On standard benchmarks, reachability verifiers applied to the transformed programs solve about as many tasks as verifiers with native support, and in the termination case the transformed composition solved more tasks than the native termination tool. The broader claim is modularity: because the transformation outputs a C program, any tool that can check reachability—verifier, tester, or fuzzer—inherits support for every specification expressible in the framework.","feed_headline":"Reachability verifiers can check termination, overflow, memory cleanup","feed_subtitle":"Instrumentation automata rewrite C programs so reachability tools can verify overflow, termination, and cleanup.","key_machinery":"The load-bearing mechanism is the instrumentation automaton (IA): a small automaton whose states carry annotations (init, loop_head, true, end) and whose transitions match CFA edges by C-expression patterns and emit operations—assertions, ghost-variable updates, nondeterministic state-saving—to be inserted before or after the matched edge. Two operators drive the transformation: the sequentialization operator ⊗ synchronously traverses the CFA and the IA and produces an instrumented CFA, and the instrumentation operator ⊎ splices those new operations back into the original C program while preserving its structure. This is what lets an arbitrary reachability verifier consume the result as ordinary C with assertions.","core_discovery":"The central discovery is that three practically important specifications—termination, no-overflow, and memory cleanup—can be reduced to reachability by a program transformation that is independent of any particular verifier, and that doing the transformation at the source level rather than inside the verifier does not cost efficiency. The reduction is exact on the supported subset: for the sequentialization operator ⊗ and the instrumentation operator ⊎, the paper asserts P |= phi iff P' |= reachability for the transformed program P'. The experimental comparison shows that reachability verifiers on transformed programs are competitive with, and sometimes better than, verifiers that natively implement the original specification, and that the framework's expressiveness extends to general liveness properties via an explicit-liveness construction.","pith_inferences":["A testable corollary the paper does not chase: since the output is plain C, coverage-guided fuzzers and concolic testers can be pointed at the instrumented program, turning any property in the IA language into a fuzzable assertion.","The framework suggests a standardization opportunity: if specification authors publish instrumentation automata as an interchange format, verifier competitions could decouple property support from algorithm tuning, making the 'specification library' a shared artifact.","The 17 benchmark tasks with hidden signed-overflow behavior found during termination experiments indicate the transformation can double as an undefined-behavior sanitizer during benchmark curation, a side effect worth exploiting deliberately.","The termination transformation's state-repetition check is inherently finite-state; extending it to heap-manipulating programs would require combining it with heap summaries or ranking-function synthesis, which the paper leaves open."],"forward_implications":["Any reachability verifier for C can be pointed at the transformed program to check termination, no-overflow, or memory cleanup, with no changes to the verifier itself.","In the experiments, the transformed reachability composition solved more termination tasks than a verifier with native termination support, and matched native no-overflow support within a few tasks.","Encoding the transformation in the input program rather than inside the verifier does not cause a systematic efficiency loss; the overhead is small relative to the 900-second time limit.","Because the framework can express general liveness as explicit liveness, any LTL property—decomposed into safety and liveness parts—can in principle be checked by a reachability-only verifier."],"supporting_citations":[{"why":"Supplies the liveness-to-safety transformation that the termination and explicit-liveness instrumentation automata are based on.","marker":"[68]"},{"why":"Introduces the observer-automaton specification language that the instrumentation automata are inspired by.","marker":"[17]"},{"why":"Provides the SLIC monitor-automaton specification language, another source of the instrumentation automaton concept.","marker":"[12]"},{"why":"Defines the competition categories and the native-support baselines against which the transformed verifiers are compared.","marker":"[15]"},{"why":"Supplies the benchmark task set and expected verdicts used for the empirical evaluation.","marker":"[16]"},{"why":"Supplies the control-flow automaton construction and the internal-transformation baseline used in the comparison.","marker":"[23]"},{"why":"Justifies the expressiveness claim by showing any LTL formula decomposes into safety and liveness parts.","marker":"[64]"}],"fun_headline_variants":["Transform C programs to verify termination, overflow, cleanup via reachability","Reachability tools verify termination, overflow, memory cleanup after transformation","Source-level transformation lets reachability verifiers handle more specs","Rewrite C programs so reachability verifiers check termination, overflow, cleanup"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The transformations are assumed to preserve the verification problem exactly—P satisfies phi if and only if the transformed program satisfies reachability—and this equivalence is not proven for the full supported subset; the termination transformation is explicitly unsound for programs with dynamic heap structures, and one memory-cleanup verdict was wrong because of function pointers.","fun_headline_variants_meta":{"raw":{"variants":["Transform C programs to verify termination, overflow, cleanup via reachability","Reachability tools verify termination, overflow, memory cleanup after transformation","Source-level transformation lets reachability verifiers handle more specs","Rewrite C programs so reachability verifiers check termination, overflow, cleanup"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000943,"raw_usage":{"total_tokens":4017,"prompt_tokens":924,"completion_tokens":3093,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":540,"completion_tokens_details":{"reasoning_tokens":3019}},"tokens_in":540,"tokens_out":3093,"duration_ms":18581,"temperature":1.0,"reasoning_tokens":3019,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T13:31:59.040785+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the termination transformation on a terminating program whose loop traverses a linked list created with malloc, so each iteration visits a fresh heap address; if the instrumented program passes the reachability check (reports no repeated state), then the transformation has wrongly certified termination. Equivalently, search the benchmark set for any program where a reachability verifier on the transformed program gives a different verdict than a trusted native verifier on the original program, and confirm the difference is caused by the transformation rather than verifier imprecision.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the liveness-to-safety transformation that the termination and explicit-liveness instrumentation automata are based on."},{"cited_title":"Beyer, A","cited_arxiv_id":null,"evidence_quote":"Introduces the observer-automaton specification language that the instrumentation automata are inspired by."},{"cited_title":"Ball and S","cited_arxiv_id":null,"evidence_quote":"Provides the SLIC monitor-automaton specification language, another source of the instrumentation automaton concept."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the benchmark task set and expected verdicts used for the empirical evaluation."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Justifies the expressiveness claim by showing any LTL formula decomposes into safety and liveness parts."}],"review_version":1}