{"id":"7128aae1-9efa-4fd6-b4ce-ac7fd8817c7e","arxiv_id":"2607.27359","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"PROGRESS embeds LLM-generated jqwik properties as search objectives in EvoSuite's DynaMOSA, detecting 58% of injected Java bugs that regression assertions miss and satisfying hard preconditions 4x more often than standalone jqwik.","lead":"PROGRESS combines properties derived from code and documentation with coverage-guided search to generate Java tests that catch bugs the current implementation's own behavior would hide. In tests on 25 Java systems it detected 58% of injected faults and reached hard property preconditions far more often than standalone property-based testing.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Regression baseline is unfair: EvoSuite's assertions are generated on the mutated program, making 0/562 trivial; a proper original-version baseline is required to support the headline claim.","rationale":"The reader's rationale explicitly identifies the same issue: 'the headline comparison to regression testing is undermined by generating the regression suite on the mutated version; that is not the standard mutation-testing baseline.' However, the reader's formal 'weakest_assumption' field focuses on property independence (oracle leakage from MUT code), not on the regression baseline. I consider the baseline flaw to be the single most load-bearing concern because it directly invalidates the strongest comparative claim (0/562 vs 328/562) and the framing that PROGRESS exposes 'bugs missed by regression-derived assertions.' If a correct baseline shows EvoSuite on the original version also kills many mutants, the paper's novelty is reduced to improving precondition reachability, not providing a new oracle paradigm. The reader's requested revision (add an original-version EvoSuite baseline) is exactly the right fix, so the conditional verdict should remain unchanged. The oracle-independence concern is real but secondary: even if properties are partly code-derived, they still serve as regression oracles against the original behavior; the empirical question is whether that differs from a proper EvoSuite baseline. The lack of repeated runs and selection bias are additional but less decisive issues.","tokens_in":15454,"tokens_out":5942,"duration_ms":65737,"concrete_test":"Rerun the RQ1 protocol with standard EvoSuite (no properties) invoked on the original, unmutated OE25 versions. Generate the minimized regression suite with assertions, then execute that suite against the 562 PIT mutants and count how many mutants are killed. Compare this kill count to PROGRESS's 328/562. If the original-version EvoSuite baseline kills a substantial fraction (e.g., >30% of mutants), the paper's claim that regression-test generation detects 'none' and lacks semantic oracle value collapses; the conclusion should be reframed as a reachability/coverage enhancement rather than an independent-oracle breakthrough.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The headline comparison in Table III is not a meaningful baseline. The paper states that 'regression-test generated by EvoSuite detects 0 of 562 injected bugs... their assertions are derived from the mutated version itself.' In mutation testing, the standard protocol is to generate tests (with assertions) on the original, unmutated program, then run those tests on mutants and count failures. By generating EvoSuite's regression suite directly on the mutated version, the authors guarantee that any behavioral change introduced by the mutant is encoded as the expected behavior, so 0/562 is a trivial consequence of the experimental design. This does not demonstrate that regression-derived assertions 'lack independent semantic value'; it demonstrates that assertions generated from the faulty version preserve the fault. The absolute detection count (328/562, 58%) and RQ2's precondition-reachability result (70/150 vs 18/150) may still be informative, but the central comparative claim — that PROGRESS detects bugs that regression-test generation misses — is unsupported until a proper original-version EvoSuite baseline is measured.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes PROGRESS, a framework that generates executable jqwik properties from code/documentation/caller-callee context via a two-stage LLM pipeline and integrates them into EvoSuite's DynaMOSA search as first-class objectives. A property-aware fitness function rewards progress through Assume preconditions and treats assertion violations as falsification. The evaluation covers 25 Java systems: RQ1 reports 328/562 injected mutants detected versus 0 for EvoSuite regression tests; RQ2 reports 70/150 hard-to-reach properties with all preconditions satisfied versus 18 for standalone jqwik; RQ3 ablates property-generation context. The paper claims that PROGRESS combines structural reachability with independent semantic oracles.","tokens_in":15715,"tokens_out":9631,"duration_ms":96836,"significance":"If the results held, PROGRESS would be a meaningful step: it operationalizes LLM-generated properties as first-class search objectives rather than post hoc oracles, and the RQ2 reachability result is a concrete improvement over random property-based testing. The engineering (parameter binding, generator hooks, fitness shaping) is detailed and the context-ablation analysis is thoughtful. However, the headline RQ1 comparison is set up so that the regression baseline cannot detect anything, and the property-generation protocol relies on a known-correct reference version that does not exist in the claimed deployment. These issues are central to the paper's contribution, so the existing evaluation does not yet support the abstract's strongest claims.","major_comments":[{"comment":"The regression-test baseline is generated on the mutated version. The paper states that 'their assertions are derived from the mutated version itself.' Under this protocol, 0/562 is a tautology: any oracle that records the mutated program's outputs as expected will pass on that program. The standard mutation-testing protocol generates the suite on the unmutated parent and then runs it on mutants. The 58%-versus-0 headline therefore does not establish that PROGRESS detects faults missed by regression-test generation. Please rerun EvoSuite on the unmutated baseline and report kills on the same 562 mutants, or explicitly reframe the claim as a comparison against regression tests generated from the buggy version and justify why that is the intended deployment.","section":"§IV-B, Table III"},{"comment":"The property-generation setup assumes a correct reference. Properties are generated from the original context bundle (including method code, documentation, and caller/callee code), and baseline-valid properties are selected by running them on the unmutated program. In the deployment the paper motivates — testing the current version for bugs already present in it — there is no unmutated reference. The LLM context includes the method's own code, so an implementation-derived property can encode buggy behavior and will still pass the baseline-valid filter. Thus the 328/562 result measures how well properties derived from a correct original detect injected changes, i.e., differential testing, not how well PROGRESS detects pre-existing bugs from a single version. A leakage experiment (generate properties from the mutated version and measure how many of the 328 kills survive) or a documentation","section":"§III-C and §IV-A"},{"comment":"The ablation is based on a single run of a stochastic LLM pipeline, and the scorer used to select MUTs is the same LLM backend as the generator. The differences between configurations (e.g., P1 328 vs. P2 325; P3 103 vs. P4 224) could be sampling noise. Reporting no variance or repeated runs makes the causal conclusions about documentation versus code context premature. Please provide repeated runs, confidence intervals, or a statistical test, and describe the sampling protocol for LLM temperature/seeds.","section":"§IV-D, Table VII"}],"minor_comments":[{"comment":"The abstract and conclusion claim that PROGRESS 'preserves structural exploration,' but no coverage comparison to vanilla EvoSuite is reported. Add coverage data or soften the claim.","section":"Abstract/§VII"},{"comment":"The paper states that a comprehensive artifact package is released, but I did not find an artifact URL or repository link. Please provide one or state how reviewers can access the package.","section":"§VII/Artifact"},{"comment":"Clarify whether the standalone jqwik timing includes the same instrumentation overhead as PROGRESS; currently the timing comparison is not apples-to-apples.","section":"§IV-C, Table VI"},{"comment":"The sentence 'The set difference JQWIK reached \\ PROGRESS reached contains only five non-comparable PROGRESS executions' is hard to parse and should be rewritten.","section":"§IV-C"},{"comment":"Minor grammar: 'regression-test generated by EvoSuite' should be 'regression-test generation' or 'regression tests generated by EvoSuite'.","section":"§IV-B"}],"recommendation":"major_revision","confidential_remarks":"The underlying idea is promising and the RQ2 result is interesting, but the current RQ1 comparison is a tautology and the property-generation protocol does not model the paper's stated deployment. Both issues are addressable within the scope of a revision: an original-version EvoSuite baseline and a leakage experiment would substantially strengthen the claims."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The interesting part of this paper is not the 328/562 number by itself; it's the way PROGRESS turns preconditions into fitness signals and materializes property inputs inside EvoSuite. The RQ2 result (70/150 vs 18/150) is the strongest evidence the integration works. The headline comparison against regression testing is unfortunately broken by the experimental setup.\n\nThe integration is genuinely new as far as I know. The two-stage LLM pipeline with origin labels, the property-aware fitness score that gives partial credit for passing preconditions, and the parameter binding are all sensible and well described. The paper ships a replication package and reports failures transparently: compilation errors, crashes, baseline-violating properties are all counted. The ablation showing that documentation plus full context gives the best validity and detection is informative.\n\nThe soft spots are in the evaluation. The 0/562 claim is trivial because the EvoSuite regression assertions are generated on the mutated version itself. Standard mutation testing generates tests on the original program and runs them on mutants; that is the only way to support the claim that regression assertions preserve faults. As it stands, the absolute 58% is still some evidence that the properties catch many mutants, but the 'none' comparison is meaningless. Second, properties are generated from the MUT's own code, not just its documentation, so calling them 'independent semantic oracles' is overstated. The baseline-valid filter only removes properties that fail on the original; it does not show the properties encode intent rather than current behavior. Third, the same LLM selects MUTs and generates properties, which introduces a mild selection bias, though the manual review helps. Finally, no repeated runs means no error bars on any of the percentages; that is a minor but real issue.\n\nThis paper is for people working on test oracle generation and search-based testing. With a proper original-version EvoSuite baseline, a clearer separation of code-derived vs doc-derived properties, and a couple of repeated runs, it would be a solid contribution. As is, it deserves a serious referee, but the revision should be expected to fix the baseline before the central comparative claim is accepted.","headline":"Useful integration of LLM properties into DynaMOSA search, but the headline 0/562 regression comparison is an artifact of generating assertions on mutated code; RQ2's reachability result is the stronger evidence.","tokens_in":16208,"tokens_out":3107,"would_cite":true,"duration_ms":29923,"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":"PROGRESS claims that intent-derived properties, embedded as first-class objectives in coverage-guided evolutionary search, expose 328/562 injected current-version bugs that regression assertions preserve.","keywords":["property-based testing","search-based test generation","regression testing","semantic oracles","precondition reachability","LLM-generated properties","mutation analysis","coverage-guided search"],"falsifier":"Generate properties while withholding the method body from the language-model context (supplying only documentation and caller/callee contracts), then run the search against the same mutant set. If kills stay near the full-context rate, the properties capture intent; if kills collapse, method code is leaking into the oracle. Alternatively, run PROGRESS on developer-confirmed bug reports and check that each reported failure is a genuine fault rather than a baseline-valid property failing for benign reasons.","tokens_in":15325,"feed_emoji":"🐞","tokens_out":9605,"duration_ms":92331,"temperature":0.7,"pith_summary":"Regression-test generation can reach faulty code but records the current, possibly wrong, behavior as the expected result; property-based testing supplies independent semantic oracles but rarely draws inputs that satisfy hard preconditions. PROGRESS's central claim is that these two can be fused: generate executable properties from documentation, caller/callee context, and method code, then inject them into a coverage-guided evolutionary test generator as first-class search objectives. A property-aware fitness reward—progress through each precondition, and a maximum reward for a failed assertion—turns hard-to-reach input gates into a gradient the search can climb. In an evaluation on 25 Java systems, PROGRESS detects 328 of 562 injected current-version bugs (58%) while regression-test generation detects none, and it satisfies all preconditions for 70 of 150 hard-to-reach properties versus 18 for standalone property-based testing. If these results hold, the practical consequence is that semantic oracles are most useful when they guide generation, not merely check completed tests.","feed_headline":"Intent-based properties catch 58% of planted bugs","feed_subtitle":"Making properties search objectives reaches 70/150 hard-to-reach states; standalone engines reach 18.","key_machinery":"The central mechanism is a property-aware fitness function over an executable property with T precondition gates: a candidate test scores 0 when the property's postcondition assertion fails; otherwise it scores T - p + 1 when p gates pass and the next gate fails, and T + 2 when the property throws unexpectedly. This turns each precondition into a step the evolutionary search can climb, so inputs that a random generator would discard become landmarks. The second pillar is a two-stage generation pipeline: natural-language behavioral claims are forced to carry evidence labels and split into single claims, then compiled into parameterized properties that must contain at least one precondition an","core_discovery":"On its own terms, the paper establishes that LLM-derived, executable behavioral properties can act as independent semantic oracles inside coverage-guided search-based test generation. The pipeline builds a per-method context bundle—focal method code, documentation, enclosing-class documentation, and resolved callers/callees—and uses a fixed two-stage language-model pipeline to turn evidence-grounded natural-language claims into compilable, parameterized properties. It then extends the underlying evolutionary search with one objective per property, a fitness score that rewards satisfying progressively more preconditions and treats an assertion violation as the best possible score, plus machin","pith_inferences":["Inference: The precondition-as-gradient idea may reduce the need for hand-written custom generators: instead of encoding the entire admissible-input domain up front, a generator can let search discover and climb the gates. A direct comparison against expert-written generators on the same property set would test this.","Inference: Because the context bundle includes the method body, oracle independence is only partial. A stress test that generates properties from documentation and caller/callee contracts while withholding the method body would separate intent-capture from implementation re-statement.","Inference: The integration pattern should transfer to other languages and property engines that expose quantified parameters, assumption gates, and assertion failures; demonstrating that would establish search-guided semantic falsification as a general technique rather than a Java-specific one.","Inference: Pairing property-guided search with relational or metamorphic properties would extend it to bugs for which no single-invocation postcondition exists; the paper's own future-work sketch on richer property forms points in this direction."],"forward_implications":["Current-version bugs can be found without a developer supplying a fixed oracle: generated intent properties kill 58% of injected mutants that regression assertions preserve.","Hard preconditions stop being a wall for property testing: 70 of 150 hard-to-reach properties become fully exercisable under PROGRESS, versus 18 for standalone generation.","Documentation and caller/callee context are load-bearing: ablations show removing them raises the invalid-property rate from 6% to as high as 42%.","Detection is uneven: semantically visible faults (negated conditions, wrong booleans, wrong return values) are caught at 71–92%, while precise boundary and arithmetic faults remain mostly missed.","A baseline-valid filter is essential: 64 of 880 generated properties already failed on the original version and had to be discarded before serving as oracles."],"fun_headline_variants":["LLM properties guide search to 58% bug detection","Search-based testing plus properties hits 70 hard states","PROGRESS: property-aware fitness snags 328 bugs","From 18 to 70: properties guide tests to deep states","LLM-generated properties catch 58% of planted bugs"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The load-bearing premise is that the generated properties express intended behavior rather than the current implementation's behavior—the context bundle includes the method's own code, and the baseline-valid filter only confirms that a property passes the original version, so it cannot by itself rule out implementation leakage.","fun_headline_variants_meta":{"raw":{"variants":["LLM properties guide search to 58% bug detection","Search-based testing plus properties hits 70 hard states","PROGRESS: property-aware fitness snags 328 bugs","From 18 to 70: properties guide tests to deep states","LLM-generated properties catch 58% of planted bugs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000245,"raw_usage":{"total_tokens":1405,"prompt_tokens":806,"completion_tokens":599,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":550,"completion_tokens_details":{"reasoning_tokens":516}},"tokens_in":550,"tokens_out":599,"duration_ms":6197,"temperature":1.0,"reasoning_tokens":516,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T08:49:33.975824+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Generate properties while withholding the method body from the language-model context (supplying only documentation and caller/callee contracts), then run the search against the same mutant set. If kills stay near the full-context rate, the properties capture intent; if kills collapse, method code is leaking into the oracle. Alternatively, run PROGRESS on developer-confirmed bug reports and check that each reported failure is a genuine fault rather than a baseline-valid property failing for benign reasons.","supporting_citations":[],"review_version":1}