Write a Blog >>

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.