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.
翻译：我们考虑了确定程序合成问题无法实现的问题(即,在特定程序搜索空间中没有解决方案 ) 。 先前关于不可实现性的工作已经开发了一些自动技术,以证明问题无法实现; 然而,这些技术都是黑箱, 意味着它们掩盖了合成问题无法实现的原因背后的推理。 在本文中, 我们提出了一个Hoare式推理系统, 称之为不现实逻辑, 以证明程序合成问题无法实现。 根据我们的知识, 不可实现性逻辑是过度赞同执行一套无限必要程序的第一个验证系统。 逻辑为建立关于不可实现性的校验证据提供了一个一般、 逻辑系统。 类似于 Hoare 逻辑如何将算法和工具背后的基本概念提取出来以证明程序的正确性, 不可实现性逻辑将先前在能够确定程序合成问题无法实现的工具中隐藏的基本概念转化为单一逻辑系统。</s>
相关内容
微信扫码咨询专知VIP会员