arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~
arXiv 2607.11811cs.PLcs.CCcs.SE

随机测试的复杂性理论

Complexity Theory of Randomised Testing

Pingshi Yu, Chengsong Tan, Nicolas Wu, Alastair Donaldson

首次发表
浏览论文内容

中文总结 AI 辅助

研究随机测试的复杂性理论,将生成器建模为图灵变换器,给出理论可生成语言与递归可枚举语言的关系,探讨高效生成及空间有界复杂性,刻画高效可生成性,还研究了基于属性测试库的相关情况。

中文摘要 AI 辅助

随机测试是软件验证中广泛使用的方法,但其理论基础薄弱。特别是,一组输入可生成的基本问题在文献和民间传说中都未得到解答。我们提出了软件测试中随机生成器的首个复杂性理论基础。将生成器建模为消耗随机位并产生字符串编码输出的图灵变换器,表明理论上可生成的语言与递归可枚举语言完全一致,这对编译器测试等可判定性边界的测试有直接影响。对于高效生成,证明多项式时间可生成语言在NP内,某些NP完全语言有高效生成器,且在标准密码学假设下,P中有语言无高效生成器。还表明空间有界复杂性是生成相关样本的自然框架。此外,刻画了高效可生成性,证明在标准假设下,没有库能从涉及合取或否定的逻辑谓词组合导出高效生成器,但受限类如NL可允许这样的编译。

英文摘要

Randomised testing is a widely-used approach to software validation, yet its theoretical foundations remain thin. In particular, the fundamental question of what it means for a set of inputs to be \emph{generable} has gone unanswered in both the literature and folklore. We present the first complexity-theoretic foundations for random generators in software testing. We model generators as Turing transducers that consume random bits and produce string-encoded outputs, and show that the theoretically generable languages coincide exactly with the recursively enumerable languages. This has direct implications for testing at the boundaries of decidability, such as compiler testing. For \emph{efficient} generation, we show that the polynomial-time generable languages lie within \textit{NP}, that certain \textit{NP}-complete languages admit efficient generators, and that -- under standard cryptographic assumptions -- there are languages in \textit{P} for which no efficient generator exists: the complexity of efficienct generation and of efficient decision are not the same. We show space-bounded complexity is the natural framework for generators producing \emph{correlated} samples, capturing methodologies such as coverage-guided fuzzing and symbolic execution. Beyond classification, we characterise efficient generability: a language has a polynomial-time generator iff it admits a \emph{certificate scheme} over a verifier -- so witness planting, the folklore technique behind generators to test SAT solvers, is in a sense the only route to efficient generation. On the design of property-based testing libraries, we prove no library can compositionally derive efficient generators from logical predicates involving conjunction or negation, under standard assumptions. However, restricted classes like \textit{NL} (equivalently, linear Datalog predicates) would admit such a compilation.

补充信息

↑