Decidable Synthesis of Programs with Uninterpreted Functions
Decidable Synthesis of Programs with Uninterpreted Functions
复制标题
DOI：
10.1007/978-3-030-53291-8_32
复制
发表时间：
2020-06-16
期刊：
影响因子：
--
通讯作者：
Viswanathan M
中科院分区：
文献类型：
--
作者：
Krogmeier P;Mathur U;Murali A;Madhusudan P;Viswanathan M
我们确定了一个可判定的合成问题的一类程序的无限大小的条件和迭代工作在无限的数据域。我们类中的程序使用未解释的函数和关系，并遵守最近确定的产生可判定验证的称为一致性的限制。我们制定了一个功能强大的语法限制（语法指导）的合成问题，连贯的未解释的程序，我们的问题是可判定的，确定其精确的复杂性，并研究了几个变种的问题。
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.
登录
查看更多内容
影响因子：
2.5
作者：
DOLEV, D;YAO, AC
通讯作者：
YAO, AC
影响因子：
0.4
作者：
Gulwani, Sumit;Polozov, Oleksandr;Singh, Rishabh
通讯作者：
Singh, Rishabh
影响因子：
2.5
作者：
Alur, Rajeev;Madhusudan, P.
通讯作者：
Madhusudan, P.
影响因子：
2.5
作者：
CHANDRA, AK;KOZEN, DC;STOCKMEYER, LJ
通讯作者：
STOCKMEYER, LJ
影响因子：
0.6
作者：
Jha, Susmit;Seshia, Sanjit A.
通讯作者：
Seshia, Sanjit A.