We consider the problem of establishing that a program-synthesis problem is
\emph{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 \emph{black-box}, meaning that they conceal the
reasoning behind \emph{why} a synthesis problem is unrealizable.
In this paper, we present a Hoare-style reasoning system, called \emph{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.
Wed 18 JanDisplayed time zone: Eastern Time (US & Canada) change
15:10 - 16:25 | Synthesis IPOPL at Grand Ballroom A Chair(s): Nadia Polikarpova University of California at San Diego | ||
15:10 25mTalk | Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions POPL DOI | ||
15:35 25mTalk | FlashFill++: Scaling Programming by Example by Cutting to the Chase POPL José Pablo Cambronero Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Daniel Perelman Microsoft, Arjun Radhakrishna Microsoft, Clint Simon Microsoft, Ashish Tiwari Microsoft DOI | ||
16:00 25mTalk | Unrealizability Logic POPL Jinwoo Kim University of Wisconsin-Madison; Seoul National University, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison DOI | ||