Syntax-Guided Synthesis

paper circuit

@book{alur2013syntax,
  title={Syntax-guided synthesis},
  author={Alur, Rajeev and Bodik, Rastislav and Juniwal, Garvit and Martin, Milo MK and Raghothaman, Mukund and Seshia, Sanjit A and Singh, Rishabh and Solar-Lezama, Armando and Torlak, Emina and Udupa, Abhishek},
  year={2013},
  publisher={IEEE}
}

Abstract

プログラム合成問題の古典的な定式化は、論理式として与えられた正しさの仕様を満たすプログラムを見つけることである。プログラム合成やプログラム最適化に関する最近の研究では、ユーザが論理的仕様を補完するために、許容される実装の空間を制約する構文テンプレートを使用できるようにすることで、多くの潜在的な利点が示されている。我々の目的は、これらの提案に共通する中核的な計算問題を、論理的な枠組みの中で特定することである。構文誘導合成問題(SyGuS)の入力は、背景理論、論理式で与えられた目的のプログラムの意味的正しさの仕様、文法で与えられた実装候補の構文的なセットからなる。計算問題は、候補式の集合から、与えられた理論の仕様を満足するような実装を見つけることである。本論文では、合成問題を解決するためのCounter-Example-guided-Inductive-Synthesis (CEGIS)戦略の3つの異なるインスタンスについて説明し、プロトタイプの実装について報告するとともに、初期のベンチマークセットでの実験結果を示す。