Hozzová, P., Kovács, L., Norman, C., & Voronkov, A. (2023). Program Synthesis in Saturation. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 307–324). Springer. https://doi.org/10.1007/978-3-031-38499-8_18
29th International Conference on Automated Deduction
en
Veranstaltungszeitraum:
1-Jul-2023 - 4-Jul-2023
-
Veranstaltungsort:
Rome, Italien
-
Umfang:
18
-
Verlag:
Springer, Cham
-
Keywords:
Program Synthesis; Saturation; Superposition; Theorem Proving
en
Abstract:
We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establish validity of this formula and discover program fragments satisfying the specification. As a result, when deriving a proof of program correctness, we also synthesize a program that is correct with respect to the given specification. We describe properties of the calculus that a saturation-based prover capable of synthesis should employ, and extend the superposition calculus in a corresponding way. We implemented our work in the first-order prover Vampire, extending the successful applicability of first-order proving to program synthesis.
en
Projekttitel:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission) Logische Komplexität und Termstruktur: P 35787-N (FWF - Österr. Wissenschaftsfonds) Doktoratskolleg: W 1255-N23 (FWF - Österr. Wissenschaftsfonds)
CC BY 4.0
