@bibtex{1910.09744,
    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.},
    Author = {Krogmeier, Paul and Mathur, Umang and Murali, Adithya and Madhusudan, P. and Viswanathan, Mahesh},
    EPrint = {arXiv:1910.09744},
    EPrintType = {arXiv},
    File = {1910.09744 - h.pdf},
    Title = {{D}ecidable {S}ynthesis of {P}rograms with {U}ninterpreted {F}unctions},
    URL = {http://arxiv.org/abs/1910.09744},
    Year = {2019},
    bdsk-url-1 = {http://arxiv.org/abs/1910.09744},
    bdsk-url-2 = {https://doi.org/10.1007/978-3-030-53291-8\_32},
    date-added = {2021-03-17 16:46:47 +0100},
    date-modified = {2021-03-17 16:46:48 +0100},
    doi = {10.1007/978-3-030-53291-8_32}
}

@bibtex{1910.09744, 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.}, Author = {Krogmeier, Paul and Mathur, Umang and Murali, Adithya and Madhusudan, P. and Viswanathan, Mahesh}, EPrint = {arXiv:1910.09744}, EPrintType = {arXiv}, File = {1910.09744 - h.pdf}, Title = {{D}ecidable {S}ynthesis of {P}rograms with {U}ninterpreted {F}unctions}, URL = {http://arxiv.org/abs/1910.09744}, Year = {2019}, bdsk-url-1 = {http://arxiv.org/abs/1910.09744}, bdsk-url-2 = {https://doi.org/10.1007/978-3-030-53291-8_32}, date-added = {2021-03-17 16:46:47 +0100}, date-modified = {2021-03-17 16:46:48 +0100}, doi = {10.1007/978-3-030-53291-8_32} }