Decidable Synthesis of Programs with Uninterpreted Functions

Paul Krogmeier; Umang Mathur; Adithya Murali; P. Madhusudan; Mahesh Viswanathan

doi:10.1007/978-3-030-53291-8_32

paper

Decidable Synthesis of Programs with Uninterpreted Functions

arXiv:1910.09744 · doi:10.1007/978-3-030-53291-8_32

Abstract

We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class use uninterpreted functions and relations, and abide by a restriction called coherence that was recently identified to yield decidable verification. We formulate a powerful grammar-restricted (syntax-guided) synthesis problem for coherent uninterpreted programs, and we show the problem to be decidable, identify its precise complexity, and also study several variants of the problem.