Record link: 
http://hdl.handle.net/20.500.12708/221409
-
Title: 
Synthesis Benchmarks for Automated Reasoning
en
Citation: 
Hajdu, M., Hozzová, P., Kovács, L., Voronkov, A., Wagner, E. M., & Žilinčík, R. S. (2025). Synthesis Benchmarks for Automated Reasoning. In V. de Paiva & P. Koepke (Eds.), Intelligent Computer Mathematics : 18th International Conference, CICM 2025 :  Brasilia, Brazil, October 6–10, 2025 :  Proceedings (pp. 21–28). Springer Nature Link. https://doi.org/10.1007/978-3-032-07021-0_2
-
Publisher DOI: 
10.1007/978-3-032-07021-0_2
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Hajdu, Márton 
Hozzová, Petra 
Kovács, Laura 
Voronkov, Andrei 
Wagner, Eva Maria 
Žilinčík, Richard Steven 
-
Organisational Unit: 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
E056-10 - Fachbereich SecInt-Secure and Intelligent Human-Centric Digital Technologies 
E056-13 - Fachbereich LogiCS 
E056-17 - Fachbereich Trustworthy Autonomous Cyber-Physical Systems 
E056-26 - Fachbereich Automated Reasoning 
-
Published in: 
Intelligent Computer Mathematics : 18th International Conference, CICM 2025 : Brasilia, Brazil, October 6–10, 2025 : Proceedings 
-
ISBN: 
978-3-032-07021-0
-
Volume: 
16136
-
DOI of the book: 
10.1007/978-3-032-07021-0
-
Date (published): 
2025
-
Event name: 
International Conference on Intelligent Computer Mathematics (CICM 2025) 
en
Event date: 
6-Oct-2025 - 10-Oct-2025
-
Event place: 
Brazil, Brazil
-
Number of Pages: 
8
-
Publisher: 
Springer Nature Link
-
Peer reviewed: 
Yes
-
Keywords: 
Automated Reasoning; Induction; Recursion; Synthesis
en
Abstract: 
Program synthesis is the task of constructing a program conforming to a given specification. We focus on deductive synthesis, and in particular on synthesis problems with specifications given as ∀∃-formulas, expressing the existence of an output corresponding to any input. So far there has been no canonical benchmark set for deductive synthesis using the ∀∃-format and supporting the so-called uncomputable symbol restriction. This work presents such a data set, composed by complementing existing benchmarks by new ones. Our data set is dynamically growing and should motivate future developments in the theory and practice of automating synthesis.
en
Project title: 
LEARN: Learning Efficient Automated Reasoning on the Net: 101213411 (European Commission) 
Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 8500 (FWF - Österr. Wissenschaftsfonds) 
Effective Formal Methods for Smart-Contract Certification: ICT22-007 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) 
-
Project (external): 
European Research Council (ERC)
Eropean Union
-
Project ID: 
10100268
0004590
-
Research Areas: 
Logic and Computation: 30%
Mathematical and Algorithmic Foundations: 30%
Computer Science Foundations: 40%
-
Science Branch: 
1020 - Informatik: 80%
1010 - Mathematik: 20%
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

130
checked on Nov 20, 2025

Download(s)

6
checked on Nov 20, 2025

Google ScholarTM

Check