{"id":"6c704210-02b5-479f-a302-267efc0bc4f1","arxiv_id":"1908.06271","paper_version":2,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"The authors implement PDR and a new PDR-based invariant generator (KIPDR) in CPAchecker, and evaluate them on 5,591 C verification tasks, finding KIPDR useful mainly for programs needing non-template invariants.","lead":"This paper studies whether a clever algorithm for proving programs correct, called PDR, can be made to work on ordinary C programs. It contributes an open implementation, a new PDR-based helper for proving loop properties, and a large benchmark comparison showing when this approach helps and when simpler methods win.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The §3 specification of lift via Craig interpolation is not logically coherent as written, so the soundness of KIPDR's auxiliary invariants is not established; the central effectiveness claim rests on this.","rationale":"I read the paper as an empirical baseline contribution whose central claim is an existential effectiveness/efficiency statement about KIPDR on invariant-generation tasks. The released artifact, the honest reporting of refuted Hypotheses 2 and 3, and the external comparison against SV-COMP verifiers are real strengths, and I do not dispute the empirical observations themselves. My concern is more foundational: the one mechanism that turns KIPDR into a property-directed invariant generator, lift via interpolation in Section 3, is not specified in a way that guarantees the lifted set C contains only genuine bad predecessors. The reader's weakest assumption focused on solver-dependent interpolation; I agree that solver choice matters, but the prior issue is that the paper never establishes the required semantic property of the interpolant or the soundness of Algorithm 1. Since the empirical results alone cannot distinguish a sound verifier from one that happens to answer correctly on the tested tasks, the ACCEPT verdict should be conditional on either a corrected and proven lift definition or a targeted check of the logged interpolants on the example programs. If that check passes, I would regard the central claim as adequately supported.","tokens_in":26767,"tokens_out":15294,"duration_ms":174220,"concrete_test":"Instrument the released KIPDR implementation to log the first CTI and the interpolant produced by MathSAT5 for eq2.c (and mod4.c), then use an independent SMT-based check to determine whether there exists a state satisfying the logged interpolant C from which the target Q still holds after k transitions (i.e., C(s_n) ∧ Inv(s_n) ∧ T(s_n,s_{n+1}) ∧ Q(s_{n+1}) is satisfiable for k=1). If such a state exists, C over-approximates the bad-predecessor set and the soundness argument fails; if no such state exists and the analogous check passes for all lifted clauses, the implementation satisfies the intended condition and the concern is limited to the paper's imprecise formal description.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Alg. 1's soundness and the claim that KIPDR is an effective invariant generator both depend on lift returning, for a CTI s, a predicate C with C(s) and C a subset of the set of k-predecessors of ¬Q. The paper states that lift can be implemented by Craig interpolation between A: s = s_n and B: Inv(s_n) ∧ ∧_{i=n}^{n+k-1}(Q(s_i)∧T(s_i,s_{i+1})) ⇒ ¬Q(s_{n+k}), \"because s is a CTI, A⇒B holds.\" This does not follow: for the CTI s, the antecedent of B (Inv plus a real k-step path to ¬Q) is true and the consequent is false, so B(s) is false and A⇒B is false. If B is instead intended as the conjunctive path-to-¬Q formula, then A∧B is satisfiable, so ordinary Craig interpolation between A and B is inapplicable. A correct formulation would need to existentially quantify the intermediate path variables or use sequence interpolants, and would need a proof that every state in the resulting interpolant really is a bad predecessor. No such proof is given for Alg. 1. Without that guarantee, an over-approximating C makes the proof obligation ¬C too strong, and the k-induction proof could use a non-invariant as an auxiliary invariant and return an unsound safety proof. The zero wrong proofs reported in Tables 3, 6, and 8 are useful empirical evidence, but they are not a substitute for this guarantee, especially on the small hand-crafted examples that carry the main conclusion.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript reports an implementation and empirical evaluation of property-directed reachability (PDR) for software verification. The authors contribute two artifacts: CPAchecker-CTIGAR, an adaptation of CTIGAR within CPAchecker, and KIPDR, an extension of k-induction that uses failed induction attempts to generate auxiliary invariants. The evaluation covers 5,591 SV-COMP 2018 tasks, a set of generated path programs, seven hand-crafted example programs, and the SV-COMP 2019 ReachSafety-Loops subcategory. The main findings are that CPAchecker-CTIGAR is a viable baseline compared with Vvt-CTIGAR, that KIPDR is less effective than data-flow-based invariant generation on the large benchmark set, and that there nevertheless exist programs (e.g., eq2.c, mod4.c, bin-suffix-5.c) for which KIPDR finds invariants that the evaluated template-based analyses cannot find, and on which KIPDR is competitive with or faster than the best SV-COMP verifiers. The paper provides a replication package and uses BenchExec for controlled measurements.","tokens_in":27052,"tokens_out":14147,"duration_ms":149667,"significance":"If the formal issue in Section 3 is repaired, this is a valuable contribution: it provides an open-source reference implementation, a careful experimental methodology on externally collected benchmarks, and an explicit, falsifiable existence claim about PDR's ability to generate nontrivial loop invariants. The paper is appropriately modest in its conclusions, explicitly refuting Hypotheses 2 and 3 and framing Hypothesis 4 as an existence statement. The replication package and the use of BenchExec resource control are clear strengths, as is the authors' willingness to report the number of wrong proofs and wrong alarms. The main weakness is formal: the central algorithm's lift operation is specified incorrectly, and no soundness theorem is supplied for Algorithm 1.","major_comments":[{"comment":"The specification of lift is not logically coherent as written. For a CTI s there is, by construction, a model of Inv(s_n) ∧ ⋀_{i=n}^{n+k-1}(Q(s_i)∧T(s_i,s_{i+1})) ∧ ¬Q(s_{n+k}) with s = s_n, so the formula B = Inv(s_n) ∧ ... ⇒ ¬Q(s_{n+k}) is false on that model; hence A⇒B does not hold and ordinary Craig interpolation between A and B is not applicable. In addition, the displayed requirement on C has the path variables s_{n+1},...,s_{n+k} under the implicit universal quantification of the implication, so it expresses that every k-step path from a C-state reaches ¬Q, not that each C-state has some k-step path to ¬Q; the latter is what the prose claims and what a CTI generalization needs. The Table 1 example is a witness to the problem: for eq2.c with k=1 and C = y≠z, a loop-body transition from a y≠z state can stay inside the loop and keep Q true, so the displayed condition is false for C. Because lines 12-14 of Algorithm 1 justify 'return false' from a violation of a proof obligation ¬C via the premise that every state in C is a k-predecessor of ¬Q, the soundness of false answers and the theoretical invariant-generation claim are unsupported. Please repair the lift contract (e.g., with an existential quantifier over the intermediate path or with sequence interpolants), prove that the produced interpolant C is a subset of the k-predecessors of ¬Q, and state the resulting soundness property of Algorithm 1.","section":"§3, lift contract and Craig-interpolation implementation"},{"comment":"Independent of the lift contract, Algorithm 1 is presented without a soundness or termination statement. The paper's conclusion treats KIPDR as an invariant generator, but the only guarantees given are the empirically observed zero wrong proofs; the operations on Oprev/O at lines 2-3 and the eager increment of k at line 33 are heuristics that are never related to a formal invariant of the algorithm. A short theorem, or at least an explicit correctness argument, stating that every predicate added to InternalInv in line 23 is a true invariant and that 'return true' in line 32 implies P holds, would be needed for the algorithm to be usable as a verification procedure beyond the reported runs. The absence of such a statement is particularly relevant because the paper advertises KIPDR as a sound auxiliary-invariant generator.","section":"§3, Algorithm 1 (global correctness)"}],"minor_comments":[{"comment":"The phrase 'rather the null hypothesis holds' is too strong; the evidence supports 'no substantial improvement on this benchmark set', not a statistical null hypothesis. Please reword or provide a significance test.","section":"§4.8, Table 3"},{"comment":"The paper should state explicitly whether the KI←KIPDR rows in Table 7 were obtained with MathSAT5, and whether any of the seven examples depended on solver-specific interpolation behavior; the text discusses this issue for Ultimate Automizer but not for KIPDR.","section":"§4.10, Table 7 and further discussion"},{"comment":"The figures omit the common header (lines 1-9) while the text refers to it; showing or explicitly referencing the header is necessary for standalone readability of the example programs.","section":"Figures 6-11"},{"comment":"Hypothesis 2 is worded as an improvement over plain k-induction, which the data (449 solved tasks vs. 0) would actually support; the experimental refutation is against data-flow-based auxiliary invariants. Please rephrase the hypothesis so that the tested claim matches the comparison actually made.","section":"§4.2, Hypothesis 2"}],"recommendation":"major_revision","confidential_remarks":"The empirical study is solid and the replication package is valuable; the Section 3 formal issue is the main blocker. I recommend major revision rather than rejection because the lift contract can be repaired with a corrected logical formulation and a proof, and the empirical existence claims are likely to survive such a repair."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nThis paper is worth reading, but for a different reason than the authors might expect. The empirical work is genuinely useful: they implement a PDR adaptation in CPAchecker, release a replication package, and run a careful evaluation on 5,591 SV-COMP tasks with BenchExec and honest reporting. They also refute two of their own hypotheses and state clearly where KIPDR loses to simple data-flow analyses. That level of openness is rare and commendable.\n\nThe novelty is KIPDR: a k-induction loop that uses failed inductive-step checks to generate proof obligations, then tries to prove those obligations by k-induction. The idea of using PDR-style CTI learning to generate auxiliary invariants is a new combination, and the paper makes a plausible 'exists' claim that on seven hand-crafted examples KIPDR solves tasks that template-based analyses cannot.\n\nThe soft spot is the theoretical specification of the lift function in Section 3. The paper says lift can be implemented by Craig interpolation between A: s = s_n and B: Inv(s_n) ∧ (∧_{i=n}^{n+k-1}(Q(s_i)∧T(s_i,s_{i+1})) ⇒ ¬Q(s_{n+k})), because 's is a CTI, and therefore A⇒B holds.' That inference is wrong. A CTI is a state with some k-step path to ¬Q; it does not imply that all k-step paths from it lead to ¬Q. The universal claim in B is stronger than what the CTI gives you. The stress-test note is correct: the interpolation-based lift is not logically justified as written. You would need to existentially quantify the intermediate states or use sequence interpolants, and then prove that the interpolant only contains bad predecessors. Without that, an over-approximating C could produce an auxiliary invariant that is false, and the k-induction loop could return a wrong proof before discovering the violation.\n\nThe empirical evidence—zero wrong proofs across the benchmarks—suggests the implementation gets away with it in practice, but the paper's central claim about KIPDR's effectiveness is loaded on this gap. The authors should fix the lift definition, or explicitly present KIPDR as a heuristic and prove that the overall loop is sound despite unsound candidates.\n\nMinor points: the solver-sensitivity (MathSAT5 vs Z3) is acknowledged but downplayed; the ReachSafety-Loops comparison in Table 8 shows KIPDR is faster on solved tasks but solves far fewer, so the 'efficiency gain' needs careful wording.\n\nBottom line: the empirical baseline deserves a serious referee, and the paper could be acceptable after major revision. As it stands, the theoretical flaw prevents me from trusting the algorithm's soundness without a better argument.\n\nBest,\n[Your name]","headline":"Solid empirical baseline for PDR-based software verification, but the theoretical justification for the new KIPDR lifting step does not hold as written; the paper deserves a serious referee but needs major revision.","tokens_in":27598,"tokens_out":10895,"would_cite":true,"duration_ms":102927,"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":"PDR proves loops that fixed templates cannot","keywords":["software verification","property-directed reachability","IC3","k-induction","invariant generation","Craig interpolation","counterexample to induction","loop invariants"],"falsifier":"Run the same KIPDR configuration with the SMT solver swapped for one whose interpolation engine returns only trivial interpolants, on the crafted tasks mod4.c and bin-suffix-5.c. If those tasks are no longer proved while the template-based configurations still time out, then the claim that PDR itself, rather than a particular solver's interpolants, computes the hard invariants is falsified.","tokens_in":26538,"feed_emoji":"🧩","tokens_out":9256,"duration_ms":83083,"temperature":0.7,"pith_summary":"Property-directed reachability (PDR) learns inductive invariants by turning failed induction attempts into proof obligations, and it has been highly successful on hardware. This paper asks whether that idea can work for ordinary C programs: it implements a standalone PDR verifier and KIPDR, an invariant generator that feeds PDR-style lemmas into k-induction, and evaluates both on 5,591 verification tasks plus seven hand-crafted programs. The headline finding is that KIPDR proves programs that template-based data-flow analyses cannot, by discovering invariants such as $y = z$ after a shared initialization, $|x| \\bmod 4 = 0$, and $(x \\& 5) = 5$ without being given a template. It also reports that on the loop-heavy benchmark subcategory, KIPDR solves fewer tasks than the best competing verifiers but uses substantially less CPU time on the tasks it does solve. A sympathetic reader would take the paper's central claim to be that PDR is a viable, sometimes faster route to exactly the class of invariants that fixed-template analyses miss.","feed_headline":"PDR proves loops that fixed templates cannot","feed_subtitle":"A property-directed k-induction variant discovers equality and modular invariants that template analyses miss, often faster.","key_machinery":"The load-bearing machinery is KIPDR, a k-induction procedure extended with a property-directed learning loop. The central operation is lift: given a concrete counterexample-to-induction state $s$, Craig interpolation between $s = s_n$ and the failed induction query produces a predicate $C$ that contains $s$ and whose every state is also a $k$-predecessor of a bad state; the negation of $C$ becomes a proof obligation. A second operation, strengthen, takes a successfully proved obligation and drops components to make it a stronger invariant before conjoining it to the internally maintained invariant. These two operations convert the standard k-induction failure--no counterexample in $k$ steps, but cannot rule out the next step--into concrete lemmas that subsequent induction checks can use.","core_discovery":"On its own terms, the paper's discovery is that the PDR ingredient can be transplanted into k-induction as a continuously-refined invariant generator, and that in this role it finds invariants outside the reach of the evaluated abstract domains. The algorithm KIPDR wraps k-induction in the PDR loop: when an induction-step check fails on the safety property or on a proof obligation, it takes the satisfying predecessor state, lifts it via Craig interpolation to a set of states that all lead to a bad state, negates that set to form a new proof obligation, and attempts to prove the obligation inductively. On the seven crafted tasks, this mechanism yields proofs for all seven, whereas the Boxes, equality-template, and parity-template data-flow combinations solve only four; on the 2019 loop benchmark it achieves lower median CPU time than the category winner on mutually solved tasks. The paper's stated conclusion is the strongest claim: PDR can be an effective and efficient technique for computing invariants that are difficult to obtain, including programs where the PDR-based approach is more efficient than the best invariant generator from the competition's loop subcategory.","pith_inferences":["The paper shows that one solver produces no suitable interpolants for some crafted tasks while another solves all seven, which implies the practical effectiveness of KIPDR is partly a property of the SMT solver's interpolation engine rather than of the algorithm alone; a solver-robustness study would be a direct next step.","Because KIPDR needed no template for $|x| \\bmod 4 = 0$ or $(x \\& 5) = 5$, a natural extension is to test it against data-flow analyses with an open-ended template family, such as arbitrary linear congruences or low-bit masks, to find where templated approaches catch up.","The paper reports that KIPDR solves some Linux-driver tasks by chaining a weaker invariant into a stronger one (for example, a reference counter greater than 0, then equal to 1); this suggests the algorithm can be used as a general lemma-discovery layer, not just a final proof engine.","Its success on the seven crafted examples is an existence proof, not a distributional statement: on the broad benchmark set data-flow remains far more effective, so the paper's practical message is to keep a template-free PDR component as a fallback rather than a replacement."],"forward_implications":["The released standalone CTIGAR implementation outperforms the only other pure PDR verifier for C (more correct results, no wrong proofs) and is positioned as the reference baseline for future PDR-for-software work.","KIPDR as an auxiliary invariant generator lets k-induction prove 449 bug-free benchmark tasks that plain k-induction cannot prove.","On the same bug-free tasks, a data-flow invariant generator based on Boxes plus simple templates proves 1,117, so KIPDR is complementary rather than dominant.","On the seven crafted tasks, KIPDR proves all seven, including the three that defeat every evaluated template combination.","On the 208-task loop benchmark, KIPDR has lower median CPU time than the best three competitors on the tasks all solve, supporting the paper's conclusion that PDR can be both effective and efficient for hard invariants."],"supporting_citations":[{"why":"Introduces PDR/IC3 and its frame structure, the algorithm that KIPDR adapts for software.","marker":"[13]"},{"why":"Supplies the k-induction with continuously-refined invariants that KIPDR extends and compares against.","marker":"[5]"},{"why":"Defines CTIGAR, the PDR-to-software adaptation that the standalone verifier implementation follows.","marker":"[12]"},{"why":"Provides Vvt, the only other pure PDR verifier for C programs and the direct baseline for the standalone implementation.","marker":"[21]"},{"why":"Defines the Boxes abstract domain, which is the strongest data-flow invariant-generation baseline in the comparison.","marker":"[22]"},{"why":"Supplies the Craig-interpolation framework used by the lift operation.","marker":"[32]"},{"why":"Reports that PDR as an interpolation engine is often too expensive, motivating the KIPDR design and the discussion of fall-back use.","marker":"[16]"},{"why":"Implements SeaHorn, the third PDR-based C verifier used for comparison.","marker":"[23]"}],"fun_headline_variants":["KIPDR: PDR-boosted k-induction finds invariants templates miss","Property-directed k-induction: more invariants, faster than template analyses","PDR as k-induction booster: finds invariants beyond template domains","PDR-embedded k-induction lowers median time on loop benchmarks","New PDR-based k-induction solver: strong invariants, efficient runs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The practical power of KIPDR rests on the SMT solver returning a precise summary of a failed induction step; if the solver can only produce trivial summaries, the learned proof obligations become useless and the algorithm's advantage over template analyses disappears.","fun_headline_variants_meta":{"raw":{"variants":["KIPDR: PDR-boosted k-induction finds invariants templates miss","Property-directed k-induction: more invariants, faster than template analyses","PDR as k-induction booster: finds invariants beyond template domains","PDR-embedded k-induction lowers median time on loop benchmarks","New PDR-based k-induction solver: strong invariants, efficient runs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001203,"raw_usage":{"total_tokens":4937,"prompt_tokens":903,"completion_tokens":4034,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":519,"completion_tokens_details":{"reasoning_tokens":3930}},"tokens_in":519,"tokens_out":4034,"duration_ms":27299,"temperature":1.0,"reasoning_tokens":3930,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T12:51:16.614864+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the same KIPDR configuration with the SMT solver swapped for one whose interpolation engine returns only trivial interpolants, on the crafted tasks mod4.c and bin-suffix-5.c. If those tasks are no longer proved while the template-based configurations still time out, then the claim that PDR itself, rather than a particular solver's interpolants, computes the hard invariants is falsified.","supporting_citations":[{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"Supplies the k-induction with continuously-refined invariants that KIPDR extends and compares against."},{"cited_title":"In: Pro c","cited_arxiv_id":null,"evidence_quote":"Provides Vvt, the only other pure PDR verifier for C programs and the direct baseline for the standalone implementation."},{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"Defines the Boxes abstract domain, which is the strongest data-flow invariant-generation baseline in the comparison."},{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"Reports that PDR as an interpolation engine is often too expensive, motivating the KIPDR design and the discussion of fall-back use."}],"review_version":1}