11
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Decidable Synthesis of Programs with Uninterpreted Functions

      Preprint

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          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 show the problem to be decidable. We identify its precise complexity, which is doubly exponential in the set of program variables and linear in the size of the grammar. The decision procedure uses tree automata which accept finite syntax trees of all correct programs. It checks that each of the infinitely many executions for a given program is correct using a finite memory streaming congruence closure algorithm. We also study variants of uninterpreted program synthesis: synthesis of transition systems with lower complexity (EXPTIME), synthesis of recursive programs, and synthesis of Boolean programs. We also show undecidability results that argue the necessity of our restrictions.

          Related collections

          Most cited references4

          • Record: found
          • Abstract: not found
          • Book Chapter: not found

          Reasoning about the past with two-way automata

            Bookmark
            • Record: found
            • Abstract: not found
            • Conference Proceedings: not found

            FIDEX: filtering spreadsheet data using examples

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              Program synthesis using abstraction refinement

                Bookmark

                Author and article information

                Journal
                21 October 2019
                Article
                1910.09744
                9ea6bb11-402c-4c3a-9a56-75b3fd39fa92

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                cs.PL cs.FL cs.LO

                Theoretical computer science,Programming languages
                Theoretical computer science, Programming languages

                Comments

                Comment on this article