Unrealizability Logic

TL;DR

This paper introduces unrealizability logic, a Hoare-style proof system that explicitly reasons about the impossibility of solving certain program-synthesis problems, providing transparent and checkable proofs.

Contribution

It presents the first proof system for overapproximating infinite imperative program sets, making unrealizability reasoning more transparent and formalized.

Findings

First proof system for unrealizability of infinite imperative programs

Provides checkable proofs for unrealizability

Unrealizability logic distills core concepts from prior black-box techniques

Abstract

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.