Skip to content

PROGRESS: Property-Guided Regression Search for Semantic Falsification

Jul 2026 · arXiv.org · Vol abs/2607.27359 · 0 citations · 19 references
Computer Science

TL;DR

This work presents PROGRESS (PROperty-Guided REgression Search for Semantic Falsification), integrating intent-driven properties into coverage-guided, search-based evolutionary test generation to reach deep program states and detect violations of intended behavior.

Abstract

Search-based regression-test generation effectively explores complex program structures, yielding high structural coverage, but its oracles are derived from the system under test: faults already present are recorded as expected behavior rather than exposed. Property-based testing offers independent semantic oracles, but depends on high-quality properties and gives little guidance for reaching deep states or satisfying selective preconditions. We present PROGRESS (PROperty-Guided REgression Search for Semantic Falsification), integrating intent-driven properties into coverage-guided, search-based evolutionary test generation to reach deep program states and detect violations of intended behavior. PROGRESS (1) extracts intent-bearing code context and uses a language-model pipeline to generate executable jqwik properties while limiting implementation leakage; (2) extends EvoSuite's DynaMOSA with a search objective and property-aware fitness function per property, rewarding progress through preconditions and prioritizing falsifying executions; and (3) binds property parameters and uses jqwik-provided generators to connect quantified inputs to evolving test sequences, steering generation toward coverage and bug-detection goals. We evaluate PROGRESS on 25 large-scale Java systems against regression-test generation, standalone property-based testing, and context ablations. PROGRESS detects 328/562 current-version bugs (58%) versus none for regression-test generation, and satisfies all preconditions for 70/150 hard-to-reach properties versus 18 for standalone jqwik. Ablations show documentation and caller/callee context are key to generating valid executable properties. PROGRESS preserves structural exploration while exposing faults missed by regression-derived assertions; we release a comprehensive artifact package.

View source

Similar papers

#artificial intelligence Preprint Aug 2026

Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

NeuroAssertion is presented, a coverage-driven assertion generation framework that combines formal trace generation, syntax-guided synthesis (SyGuS), and an agent-inspired refinement process within a unified framework that delivers around 2X more assertions and about 2X higher mutation coverage than traditional asserti...

Zhi-Yuan Yan, Ziyue Zheng, Hongce Zhang · 0 citations
Preprint Aug 2026

Neuro-Symbolic Proof-of-Vulnerability Generation with Open-Weight Models

POVGEN, a low-cost neuro-symbolic framework that makes PoV generation cost-effective via semantic focusing and LLM-guided constraint reasoning using open-weight models, and fine-tuned open-weight models match frontier commercial LLMs on key sub-tasks while running locally at no per-sample API cost.

Yu Nong, Hai-Peng Cai · 0 citations
#natural language process... Preprint Aug 2026

SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs

SKILLFORGE is introduced, a framework that decomposes formal code synthesis into a library of atomic, reusable skills, each targeting a specific subtask such as specification inference, body synthesis, invariant generation, error diagnosis, or targeted repair, and defined by a prompt template, tool binding, and decidab...

Yan-Ming Liu, Xinyue Peng, Jiannan Cao et al. · 0 citations
Aug 2026

CGARF: a causality-guided framework for reliable automated program repair

Results suggest that causal-aware reasoning and stability-oriented design can improve the effectiveness of LLM-based APR, a causality-guided multi-agent repair framework that improves the repair stage of existing LLM-based localization pipelines.

Lei Yuan, Shaohua Liu, Yu Wang et al. · 0 citations

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.