Decidable Synthesis of Programs with Uninterpreted Functions

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 y...

Descripción completa

Detalles Bibliográficos
Autores principales: Krogmeier, Paul, Mathur, Umang, Murali, Adithya, Madhusudan, P., Viswanathan, Mahesh
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363337/
http://dx.doi.org/10.1007/978-3-030-53291-8_32
_version_ 1783559643490942976
author Krogmeier, Paul
Mathur, Umang
Murali, Adithya
Madhusudan, P.
Viswanathan, Mahesh
author_facet Krogmeier, Paul
Mathur, Umang
Murali, Adithya
Madhusudan, P.
Viswanathan, Mahesh
author_sort Krogmeier, Paul
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7363337
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73633372020-07-16 Decidable Synthesis of Programs with Uninterpreted Functions Krogmeier, Paul Mathur, Umang Murali, Adithya Madhusudan, P. Viswanathan, Mahesh Computer Aided Verification Article 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. 2020-06-16 /pmc/articles/PMC7363337/ http://dx.doi.org/10.1007/978-3-030-53291-8_32 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Krogmeier, Paul
Mathur, Umang
Murali, Adithya
Madhusudan, P.
Viswanathan, Mahesh
Decidable Synthesis of Programs with Uninterpreted Functions
title Decidable Synthesis of Programs with Uninterpreted Functions
title_full Decidable Synthesis of Programs with Uninterpreted Functions
title_fullStr Decidable Synthesis of Programs with Uninterpreted Functions
title_full_unstemmed Decidable Synthesis of Programs with Uninterpreted Functions
title_short Decidable Synthesis of Programs with Uninterpreted Functions
title_sort decidable synthesis of programs with uninterpreted functions
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363337/
http://dx.doi.org/10.1007/978-3-030-53291-8_32
work_keys_str_mv AT krogmeierpaul decidablesynthesisofprogramswithuninterpretedfunctions
AT mathurumang decidablesynthesisofprogramswithuninterpretedfunctions
AT muraliadithya decidablesynthesisofprogramswithuninterpretedfunctions
AT madhusudanp decidablesynthesisofprogramswithuninterpretedfunctions
AT viswanathanmahesh decidablesynthesisofprogramswithuninterpretedfunctions

Ejemplares similares