<div class="csl-bib-body">
<div class="csl-entry">Hozzová, P., Kovács, L., Norman, C., & Voronkov, A. (2023). Program Synthesis in Saturation. In B. Pientka & C. Tinelli (Eds.), <i>Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings</i> (pp. 307–324). Springer. https://doi.org/10.1007/978-3-031-38499-8_18</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/192768
-
dc.description.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
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
Program Synthesis
en
dc.subject
Saturation
en
dc.subject
Superposition
en
dc.subject
Theorem Proving
en
dc.title
Program Synthesis in Saturation
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.relation.publication
Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings
-
dc.contributor.affiliation
University of California, Berkeley, United States of America (the)
-
dc.contributor.affiliation
Manchester University, United States of America (the)
-
dc.contributor.editoraffiliation
McGill University, Canada
-
dc.contributor.editoraffiliation
University of Iowa, United States of America (the)
-
dc.relation.isbn
978-3-031-38498-1
-
dc.relation.doi
10.1007/978-3-031-38499-8
-
dc.relation.issn
0302-9743
-
dc.description.startpage
307
-
dc.description.endpage
324
-
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.relation.grantno
P 35787-N
-
dc.relation.grantno
W 1255-N23
-
dc.rights.holder
(c) the Authors 2023
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
tuw.booktitle
Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings
-
tuw.container.volume
14132
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.project.title
Logische Komplexität und Termstruktur
-
tuw.project.title
Doktoratskolleg
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publisher.doi
10.1007/978-3-031-38499-8_18
-
dc.identifier.libraryid
AC17202941
-
dc.description.numberOfPages
18
-
tuw.author.orcid
0000-0003-0845-5811
-
tuw.author.orcid
0000-0002-8299-2714
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
tuw.editor.orcid
0000-0002-2549-4276
-
tuw.event.name
29th International Conference on Automated Deduction
en
tuw.event.startdate
01-07-2023
-
tuw.event.enddate
04-07-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Rome
-
tuw.event.country
IT
-
tuw.event.presenter
Hozzová, Petra
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.mimetype
application/pdf
-
item.openairetype
conference paper
-
item.cerifentitytype
Publications
-
item.grantfulltext
open
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openaccessfulltext
Open Access
-
item.fulltext
with Fulltext
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
FWF - Österr. Wissenschaftsfonds
-
crisitem.project.funder
FWF - Österr. Wissenschaftsfonds
-
crisitem.project.grantno
ERC Consolidator Grant 2020
-
crisitem.project.grantno
P 35787-N
-
crisitem.project.grantno
W 1255-N23
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192 - Institut für Logic and Computation
-
crisitem.author.dept
University of California, Berkeley
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
