Skip to content
Log in
Sponsored AI Networking Cookbook: Practical recipes for AI-assisted network automation and development AI Networking Cookbook: Practical recipes for AI-assisted network automation and development

PROGRESS: Property-Guided Regression Search for Semantic Falsification

D. Mo Noshin Ulfat Matthew B. Dwyer Soneya Binta Hossain
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.

DOI arXiv Semantic Scholar
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 assertion mining methods.

Zhiyuan 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, Haipeng 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 decidable success criterion.

Yanming 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
Preprint Aug 2026

Explanation-Guided Metamorphic Testing of Specialized Language Models: An Empirical Study

\head{Background} Task-specialized language models are increasingly integrated into software engineering workflows to support vertical-domain activities such as issue triaging, document classification, and automated analysis. Despite their adoption, there is limited empirical evidence on how to test their robustness and detect brittle behaviors under semantics-preserving input transformations. \head{Aims} This paper investigates whether explainability-guided metamorphic testing can improve the effectiveness and validity of robustness testing for specialized language models compared to heuristic mutation strategies. \head{Method} We conduct a large-scale empirical study of explanation-guided metamorphic testing across three datasets, four model architectures, and 20 testing configurations derived from combinations of attribution methods and mutation strategies. The evaluated configurations combine attribution-based token prioritization, LLM-driven mutation, and automated semantic verification to generate linguistically valid test variants. We assess failure discovery capability, semantic validity, and testing efficiency against heuristic baselines. \head{Results} Explanation-guided metamorphic testing generates 2.30$\times$ more verified failure-inducing test cases than heuristic mutation strategies. Semantic verification substantially improves mutation validity and achieves high label-preservation precision among gate-accepted variants according to human annotation. The study further reveals systematic shortcut behaviors across models, including over-reliance on named entities and formatting cues. \head{Conclusions} The results provide evidence that explanation-guided metamorphic testing is an effective and practical approach for empirically evaluating the robustness of task-specialized language models used in vertical AI applications.

Xingcheng Chen, Mehmet Besenk, Andrea Stocco · 0 citations

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