Decidable Synthesis of Programs with Uninterpreted Functions
| Autor: | Paul Krogmeier, Mahesh Viswanathan, P. Madhusudan, Umang Mathur, Adithya Murali |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
050101 languages & linguistics
Class (set theory) Theoretical computer science Computer science Data domain 05 social sciences 02 engineering and technology Coherence (statistics) Decidability TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering Computer Science::Programming Languages 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Hardware_REGISTER-TRANSFER-LEVELIMPLEMENTATION |
| Zdroj: | Computer Aided Verification ISBN: 9783030532901 CAV (2) |
| DOI: | 10.1007/978-3-030-53291-8_32 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|