一句话：提出可复用指称语义理论，刻画无限程序集合验证的表达力与组合性，并导出首个可靠且相对完备的 Hoare 式逻辑。
程序合成等应用常需证明文法所描述的无限程序集合中所有程序都满足某性质，但现有验证框架在集合含循环时只能过近似程序行为，两个 Hoare 式逻辑也因此失去相对完备性。本文证明：要组合式验证无限程序集合的简单性质，必须跟踪无界多次执行下不同的程序行为，这一信息既是必要条件也是充分条件。作者建立通用、可复用的指称语义理论，用于建模无限程序集合上验证技术的表达力与组合性，并构造出捕获简单性质的最小组合语义。基于该语义，他们导出首个针对无限程序集合的可靠且相对完备的 Hoare 式逻辑。该工作为设计最小复杂度、可组合的程序集合验证技术提供了理论方法。
Applications like program synthesis sometimes require proving that a property holds for all of the infinitely many programs described by a grammar—i.e., an inductively defined set of programs. Current verification frameworks overapproximate programs’ behavior when sets of programs contain loops, including two Hoare-style logics that fail to be relatively complete when loops are allowed. In this work, we prove that compositionally verifying simple properties for infinite sets of programs requires tracking distinct program behaviors over unboundedly many executions. Tracking this information is both necessary and sufficient for verification. We prove this fact in a general, reusable theory of denotational semantics that can model the expressivity and compositionality of verification techniques over infinite sets of programs. We construct the minimal compositional semantics that captures simple properties of sets of programs and use it to derive the first sound and relatively complete Hoare-style logic for infinite sets of programs. Thus, our methods can be used to design minimally complex, compositional verification techniques for sets of programs.
@article{paperbot3152,
title = {Semantics of Sets of Programs},
author = {Jinwoo Kim and Shaan Nagy and Thomas Reps and Loris D'Antoni},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720515}
}