Generative transformations and patterns in LLM-native approaches for software verification and falsification

TL;DR

This paper introduces a transformation-centric lens to study LLM-native software engineering for verification and falsification, arguing that treating prompt-driven interactions as discrete generative transformations enables principled analysis and modular design. Through a systematic mapping of over 100 proposals, the authors extract 284 transformations across 111 studies, organize them into a hierarchical taxonomy, and identify inter-transformation patterns that resemble software design patterns. They show how transformation types align with SE problems (e.g., unit testing, fuzzing, vulnerability detection) and reveal common motifs such as Generate and Fix and Build Model, shedding light on compositional strategies and gaps. The work provides a foundational vocabulary and taxonomy to support benchmarks, transformation-specialized tooling, and ex-ante methodologies for reliable, modular LLM-native verification workflows, with implications for future engineering practices in this rapidly evolving domain.

Abstract

The emergence of prompting as the dominant paradigm for leveraging Large Language Models (LLMs) has led to a proliferation of LLM-native software, where application behavior arises from complex, stochastic data transformations. However, the engineering of such systems remains largely exploratory and ad-hoc, hampered by the absence of conceptual frameworks, ex-ante methodologies, design guidelines, and specialized benchmarks. We argue that a foundational step towards a more disciplined engineering practice is a systematic understanding of the core functional units--generative transformations--and their compositional patterns within LLM-native applications. Focusing on the rich domain of software verification and falsification, we conduct a secondary study of over 100 research proposals to address this gap. We first present a fine-grained taxonomy of generative transformations, abstracting prompt-based interactions into conceptual signatures. This taxonomy serves as a scaffolding to identify recurrent transformation relationship patterns--analogous to software design patterns--that characterize solution approaches in the literature. Our analysis not only validates the utility of the taxonomy but also surfaces strategic gaps and cross-dimensional relationships, offering a structured foundation for future research in modular and compositional LLM application design, benchmarking, and the development of reliable LLM-native systems.

Figures (29)

• Figure 1: An abstract execution of ChatTESTER ChatTester modeled using our conceptual framework. This Bayesian network depicts data flow through the system, where variables represent either inputs (FocalMethod) or outputs from transformations. Generative transformations (labeled with types like IntentCorresponding-Test-Generation) produce stochastic variables through LLM-mechanized processes, while algorithmic transformations produce deterministic variables (double-circled, e.g., CompilationErrors). Edges denote the conceptual input signature of each transformation; for instance, UnitTest(0) depends on Signature and Intent according to the distribution of an IntentCorresponding-Test-Generation transformation. The model reveals two key inter-transformation patterns: Use Verbalized SW Entity (reasoning via intent rather than code) and Generate & Fix (iterative correction using compilation errors).
• Figure 2: Overview of the SE problems considered in this paper, and the tools corresponding to each of them. Framed tools are the ASE'24 ones, that were added at the validation step.
• Figure 3: Taxonomy based on the transformation types found in the reported papers.
• Figure 4: Number of transformations using each prompting technique or combination of prompting techniques, aggregated by transformation category.
• Figure 5: Test Generation. .