Scholarlink

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 \(\forall \exists \) -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 \(\forall \exists \) -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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Synthesis Benchmarks for Automated Reasoning

  • 会议论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年

查看全文
  • Márton Hajdu,
  • Petra Hozzová,
  • Laura Kovács,
  • Andrei Voronkov,
  • Eva Maria Wagner,
  • Richard Steven Žilinčík

摘要

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 \(\forall \exists \) -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 \(\forall \exists \) -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.