Decidable Synthesis of Programs with Uninterpreted Functions

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

doi:10.1007/978-3-030-53291-8_32

Decidable Synthesis of Programs with Uninterpreted Functions

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

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
Editors	Shuvendu K. Lahiri, Chao Wang
Publisher	Springer
Pages	634-657
Number of pages	24
ISBN (Print)	9783030532901
DOIs	https://doi.org/10.1007/978-3-030-53291-8_32
State	Published - 2020
Event	32nd International Conference on Computer Aided Verification, CAV 2020 - Los Angeles, United States Duration: Jul 21 2020 → Jul 24 2020

Publication series

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

Conference

Conference	32nd International Conference on Computer Aided Verification, CAV 2020
Country/Territory	United States
City	Los Angeles
Period	7/21/20 → 7/24/20

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-030-53291-8_32License: CC BY

Library availability

Discover UIUC Full Text

Cite this

Krogmeier, P., Mathur, U., Murali, A., Madhusudan, P., & Viswanathan, M. (2020). Decidable Synthesis of Programs with Uninterpreted Functions. In S. K. Lahiri, & C. Wang (Eds.), Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings (pp. 634-657). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12225 LNCS). Springer. https://doi.org/10.1007/978-3-030-53291-8_32

Decidable Synthesis of Programs with Uninterpreted Functions. / Krogmeier, Paul; Mathur, Umang; Murali, Adithya et al.
Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. ed. / Shuvendu K. Lahiri; Chao Wang. Springer, 2020. p. 634-657 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12225 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Krogmeier, P, Mathur, U, Murali, A, Madhusudan, P & Viswanathan, M 2020, Decidable Synthesis of Programs with Uninterpreted Functions. in SK Lahiri & C Wang (eds), Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12225 LNCS, Springer, pp. 634-657, 32nd International Conference on Computer Aided Verification, CAV 2020, Los Angeles, United States, 7/21/20. https://doi.org/10.1007/978-3-030-53291-8_32

Krogmeier P, Mathur U, Murali A, Madhusudan P , Viswanathan M. Decidable Synthesis of Programs with Uninterpreted Functions. In Lahiri SK, Wang C, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. Springer. 2020. p. 634-657. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-53291-8_32

Krogmeier, Paul ; Mathur, Umang ; Murali, Adithya et al. / Decidable Synthesis of Programs with Uninterpreted Functions. Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. editor / Shuvendu K. Lahiri ; Chao Wang. Springer, 2020. pp. 634-657 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9be39b4aa154402a8fda1e01f753c12e,

title = "Decidable Synthesis of Programs with Uninterpreted Functions",

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.",

author = "Paul Krogmeier and Umang Mathur and Adithya Murali and P. Madhusudan and Mahesh Viswanathan",

note = "Paul Krogmeier and Mahesh Viswanathan are partially supported by NSF CCF 1901069. Umang Mathur is partially supported by a Google PhD Fellowship.; 32nd International Conference on Computer Aided Verification, CAV 2020 ; Conference date: 21-07-2020 Through 24-07-2020",

year = "2020",

doi = "10.1007/978-3-030-53291-8_32",

language = "English (US)",

isbn = "9783030532901",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "634--657",

editor = "Lahiri, {Shuvendu K.} and Chao Wang",

booktitle = "Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings",

address = "Germany",

}

TY - GEN

T1 - Decidable Synthesis of Programs with Uninterpreted Functions

AU - Krogmeier, Paul

AU - Mathur, Umang

AU - Murali, Adithya

AU - Madhusudan, P.

AU - Viswanathan, Mahesh

N1 - Paul Krogmeier and Mahesh Viswanathan are partially supported by NSF CCF 1901069. Umang Mathur is partially supported by a Google PhD Fellowship.

PY - 2020

Y1 - 2020

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

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

UR - http://www.scopus.com/inward/record.url?scp=85089221281&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85089221281&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-53291-8_32

DO - 10.1007/978-3-030-53291-8_32

M3 - Conference contribution

AN - SCOPUS:85089221281

SN - 9783030532901

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 634

EP - 657

BT - Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings

A2 - Lahiri, Shuvendu K.

A2 - Wang, Chao

PB - Springer

T2 - 32nd International Conference on Computer Aided Verification, CAV 2020

Y2 - 21 July 2020 through 24 July 2020

ER -

Decidable Synthesis of Programs with Uninterpreted Functions

Abstract

Publication series

Conference

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this