一句话：提出首个用于证明程序合成问题不可实现（无解）的 Hoare 风格证明系统，可对无限程序集的执行进行上近似。
该论文研究如何证明一个程序合成问题在给定程序搜索空间中不可实现（即无解）。已有自动技术虽能判定不可实现性，但都是黑盒，隐藏了推理依据。为此，作者提出一种 Hoare 风格的推理系统，称为不可实现性逻辑（unrealizability logic）。据称这是首个对无限个命令式程序集合的执行进行上近似的证明系统，提供通用逻辑框架来构造可检查的不可实现性证明。其目标类似 Hoare 逻辑提炼程序正确性证明背后的基本概念：将先前工具中隐含的概念统一为一个逻辑系统。
We consider the problem of establishing that a program-synthesis problem is unrealizable (i.e., has no solution in a given search space of programs). Prior work on unrealizability has developed some automatic techniques to establish that a problem is unrealizable; however, these techniques are all black-box , meaning that they conceal the reasoning behind why a synthesis problem is unrealizable. In this paper, we present a Hoare-style reasoning system, called unrealizability logic for establishing that a program-synthesis problem is unrealizable. To the best of our knowledge, unrealizability logic is the first proof system for overapproximating the execution of an infinite set of imperative programs. The logic provides a general, logical system for building checkable proofs about unrealizability. Similar to how Hoare logic distills the fundamental concepts behind algorithms and tools to prove the correctness of programs, unrealizability logic distills into a single logical system the fundamental concepts that were hidden within prior tools capable of establishing that a program-synthesis problem is unrealizable.