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
Event date:
1-Jul-2023 - 4-Jul-2023
-
Event place:
Rome, Italy
-
Number of Pages:
18
-
Publisher:
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
Project title:
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
