Decidable Synthesis of Programs with Uninterpreted Functions
Programming Languages
2020-07-24 v2 Formal Languages and Automata Theory
Logic in Computer Science
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.
Cite
@article{arxiv.1910.09744,
title = {Decidable Synthesis of Programs with Uninterpreted Functions},
author = {Paul Krogmeier and Umang Mathur and Adithya Murali and P. Madhusudan and Mahesh Viswanathan},
journal= {arXiv preprint arXiv:1910.09744},
year = {2020}
}