TY - GEN
T1 - Decidable Synthesis of Programs with Uninterpreted Functions
AU - Krogmeier, Paul
AU - Mathur, Umang
AU - Murali, Adithya
AU - Madhusudan, P.
AU - Viswanathan, Mahesh
N1 - Funding Information:
Paul Krogmeier and Mahesh Viswanathan are partially supported by NSF CCF 1901069. Umang Mathur is partially supported by a Google PhD Fellowship.
Publisher Copyright:
© 2020, The Author(s).
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85089221281&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85089221281&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-53291-8_32
DO - 10.1007/978-3-030-53291-8_32
M3 - Conference contribution
AN - SCOPUS:85089221281
SN - 9783030532901
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 634
EP - 657
BT - Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
A2 - Lahiri, Shuvendu K.
A2 - Wang, Chao
PB - Springer
T2 - 32nd International Conference on Computer Aided Verification, CAV 2020
Y2 - 21 July 2020 through 24 July 2020
ER -