PV1 ⊧ NOPEgiven a syntax-guided synthesis problem, checks whether it is realisable

Tool to determine whether a syntax-guided synthesis problem is unrealizable (i.e. has no solution).

Application domain/field

• Program synthesis
• Syntax-guided synthesis (SyGuS)

Type of tool

Property checker?

Expected input

SyGuS problem

Expected output

realizable or unrealizable. It is also possible that a time out occurs.

Internals

Unrealizability problem: Given syntax-guided synthesis (SyGuS), establish whether the problem is unrealizable (i.e. has no solution) Given an unrealizability problem of the form $sy=(\psi ,G)$, it returns unrealizable if no expression-tree in $L(G)$ satisfies $\psi$. If it returns realizable, some $e\in L(G)$ satisfies $\psi$. Uses SeaHorn, ESolver, Z3.

Comments

There exist SyGuS problems for which the algorithm cannot prove unrealizability (i.e. the algorithm is incomplete) but the authors argue that it works for many SyGuS instances.