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.

翻译：我们考虑建立程序综合问题不可实现性（即在给定的程序搜索空间中无解）的问题。关于不可实现性的前期工作已开发出一些自动技术来证明问题不可实现；然而这些技术均为黑箱方法，即它们隐藏了综合问题为何不可实现背后的推理过程。本文提出一个称为不可实现性逻辑的霍尔式推理系统，用于建立程序综合问题的不可实现性。据我们所知，不可实现性逻辑是首个用于超近似无限指令程序集执行的证明系统。该逻辑提供了一个通用的逻辑系统，用于构建关于不可实现性的可验证证明。正如霍尔逻辑提炼出证明程序正确性的算法与工具背后的基本概念，不可实现性逻辑将一个单一的逻辑系统提炼出了先前能够建立程序综合问题不可实现性的工具中所隐藏的基本概念。