@inproceedings{CAV2020UninterpretedSynthesis,
    author = {Krogmeier, Paul and Mathur, Umang and Murali, Adithya and Madhusudan, P. and Viswanathan, Mahesh},
    title = {Decidable Synthesis of Programs with Uninterpreted Functions},
    year = {2020},
    isbn = {978-3-030-53290-1},
    publisher = {Springer-Verlag},
    address = {Berlin, Heidelberg},
    url = {https://doi.org/10.1007/978-3-030-53291-8_32},
    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.},
    booktitle = {Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II},
    pages = {634–657},
    numpages = {24},
    location = {Los Angeles, CA, USA}
}