Decidable Synthesis of Programs with Uninterpreted Functions

Paul Krogmeier, Umang Mathur, Adithya Murali, P. Madhusudan, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
EditorsShuvendu K. Lahiri, Chao Wang
PublisherSpringer
Pages634-657
Number of pages24
ISBN (Print)9783030532901
DOIs
StatePublished - 2020
Event32nd International Conference on Computer Aided Verification, CAV 2020 - Los Angeles, United States
Duration: Jul 21 2020Jul 24 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12225 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference32nd International Conference on Computer Aided Verification, CAV 2020
CountryUnited States
CityLos Angeles
Period7/21/207/24/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Decidable Synthesis of Programs with Uninterpreted Functions'. Together they form a unique fingerprint.

Cite this