Unrealizability Logic

Jinwoo Kim, Loris D'Antoni, Thomas Reps

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…