Decidable synthesis of programs with uninterpreted functions

DOI10.1007/978-3-030-53291-8_32MaRDI QIDQ2226763zbMATH OpenOpenAlexFDO

Authors Paul Krogmeier, Umang Mathur, Adithya Murali, Parthasarathy Madhusudan, Mahesh Viswanathan

Publication date 9 February 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1910.09744

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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.

Recommendations

• What's decidable about program verification modulo axioms?
• Synthesizing reactive programs
• From program verification to program synthesis
• scientific article; zbMATH DE number 4049027
• Using program synthesis for program analysis

Cited in

(6)

• Using program synthesis for program analysis
• What's decidable about program verification modulo axioms?
• Temporal stream logic modulo theories
• Church synthesis on register automata over linearly ordered data domains
• Trace Abstraction-Based Verification for Uninterpreted Programs
• Church synthesis on register automata over linearly ordered data domains

This page was built for publication: Decidable synthesis of programs with uninterpreted functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2226763)