一句话：把随机输入生成重构为抽象域元素的迭代精化，用运行时抽象解释实现轻量约束求解与传播，从而对复杂前置条件的 C 程序做随机测试。
基于属性的 C 程序测试可由分离逻辑规范自动合成随机输入生成器，但现有工具 Bennet 的随机回溯搜索在指针算术等复杂约束下难以求解。本文把生成重构为抽象域元素的迭代精化，采样具体值即最后一步精化：运行时做抽象解释得到抽象元素，从而获得轻量的约束求解与传播。作者提出推测式精化、纠正式精化与级联传播三种策略，并在单子语义以抽象域为参数的生成器 DSL 中形式化，实现工具 Lucas。在十六个工作负载（Bennet 的六个案例、六个位置无关数据结构、四个空闲链表分配器）上，精化配置在四个分配器和两个位置无关数据结构中发现了 Bennet 式随机回溯遗漏的缺陷。
Property-based testing of C programs can be automated by synthesizing random input generators from separation-logic specifications. Existing work in this space, such as the Bennet testing tool, uses randomized backtracking search, generating random values and checking them against constraints, backtracking on failure. Although this approach performs well on simple recursive heap structures, it struggles as constraints grow more complex, particularly when they involve pointer arithmetic—as, for example, in the many forms of specialized storage allocators that arise in low-level systems software. Existing work uses targeted optimizations and heuristics to satisfy specific classes of constraints, but this requires continual expansion as new special cases arise, resulting in complex tools. We reframe generation as the iterative refinement of abstract domain elements, where sampling a concrete value is the final refinement. By applying abstract interpretation at runtime to obtain an abstract element, we obtain a lightweight form of constraint solving and propagation that enables randomized testing of programs with complex preconditions. We identify three strategies for applying abstract interpretation: (1) speculative refinement, refining abstract elements before sampling based on immediately following constraints, (2) corrective refinement, calculating “desired” abstract elements from information gleaned from failed constraints, and (3) cascading propagation, propagating information from failures to components of compound expressions. We formalize these ideas in a generator DSL whose monadic semantics are parametric over abstract domains. We implement this DSL in a new tool called Lucas and evaluate it on sixteen workloads: the six original case studies from the Bennet paper, six position-independent data structures, and four free-list allocators. Comparing configurations with and without refinement, we find that refinement finds bugs in all four allocators and in two of the position-independent data structures that Bennet-style random backtracking fails to find.
@article{paperbot12099,
title = {Random Testing via Runtime Abstract Interpretation},
author = {Zain K Aamer and Benjamin C. Pierce},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839513}
}