POPL 2020 (series) / Student Research Competition /
Proving Unrealizability for Imperative Syntax-Guided Synthesis Problems
We focus on proving unrealizability of SyGuS problems for imperative programs with loops. We identify several difficulties that arise from dealing with imperative programs, present our solutions to them, and also implement our solutions in a prototype tool that succeeds in proving unrealizability for simple benchmarks including loops.