一句话：提出首个 Unrealizability Logic 证明合成算法 Wuldo，以语法驱动方式自动验证无限程序集并复用非终结符摘要。
验证由正则树文法定义的（可能无限）程序集，对程序合成、动态加载代码与并发代码验证均有价值，但已有技术范围受限，生成的信息难以解释和复用。Unrealizability Logic（UL）是首个针对程序集的 Hoare 风格证明系统，用非终结符摘要刻画递归非终结符。本文提出首个 UL 证明合成算法并实现为 Wuldo：将 UL 规则应用决策与摘要合成/检查解耦，以完全语法驱动的方式计算证明结构。实验表明，给定摘要时 Wuldo 能证明现有工具无法处理的问题，包括无限程序在无限输入上的行为；部分情况下可自动合成摘要；复用已证摘要使验证速度达到从头证明的 1.96 倍。
Automated verification of all members of a (potentially infinite) set of programs has the potential to be useful in program synthesis, as well as in verification of dynamically loaded code, concurrent code, and language properties. Existing techniques for verification of sets of programs are limited in scope and unable to create or use interpretable or reusable information about sets of programs. The consequence is that one cannot learn anything from one verification problem that can be used in another. Unrealizability Logic (UL), proposed by Kim et al. as the first Hoare-style proof system to prove properties over sets of programs (defined by a regular tree grammar), presents a theoretical framework that can express and use reusable insight. In particular, UL features nonterminal summaries —inductive facts that characterize recursive nonterminals (analogous to procedure summaries in Hoare logic). In this work, we design the first UL proof synthesis algorithm, implemented as Wuldo . Specifically, we decouple the problem of deciding how to apply UL rules from the problem of synthesizing/checking nonterminal summaries by computing proof structure in a fully syntax-directed fashion. We show that Wuldo , when provided nonterminal summaries, can express and prove verification problems beyond the reach of existing tools, including establishing how infinitely many programs behave on infinitely many inputs. In some cases, Wuldo can even synthesize the necessary nonterminal summaries. Moreover, Wuldo can reuse previously proven nonterminal summaries across verification queries, making verification 1.96 times as fast as when summaries are instead proven from scratch.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{NagyKRD24,
title = {Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs},
author = {Shaan Nagy and Jinwoo Kim and Thomas Reps and Loris D’Antoni},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689715}
}