@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00174528,
 author = {木村, 悠介 and 石山, 薫太郎 and 藤田, 昌宏 and Yusuke, Kimura and Kuntaro, Ishiyama and Masahiro, Fujita},
 book = {DAシンポジウム2016論文集},
 issue = {12},
 month = {Sep},
 note = {従来から入出力の論理的使用からプログラムを合成する研究が進められてきている．これに対して最近，合成対象プログラムに対し，シンタックス上の制限を加えることで探索範囲を絞り，限られた数の入出力組のみで自動合成する手法が注目されている．比較的少数の入出力組からプログラムを合成できるので，仕様の詳細は不明だが処理内容の概要が分かっている場合などに適用できる．本研究ではこの従来手法を拡張し，テンプレートを利用した合成手法を提案する．当手法では，プログラム中の何カ所かの不明な部分に対して矛盾のない解を自動的に生成することができる．C 言語用の有界モデル検査ツールを利用した実装を利用して，数 100 行規模の暗号化プログラムや制御ソフトウェアを合成した結果について報告する．, Research has been done on what is called ”Program Synthesis,” where a program is synthesized from a given logical specification between inputs and outputs. Recently, a syntax restricted synthesis method that uses relatively few input/output vectors has been suggested, and it has drawn a great deal of positive attention. In this method, the search space of the synthesized program is restricted by setting the limitations on the scope of the program syntax. This can be applied in case where the designers cannot fully specify the program but understand the general flow of the target program. By extending this method, we introduce a new program synthesis method that uses a program template. Our proposed method can automatically generate a correct solution for a given partially vacant program. The method has been implemented on a bounded model checker for C, and the experimental results of the encryption program and the control program, written in hundreds of lines of C code, are presented.},
 pages = {62--67},
 publisher = {情報処理学会},
 title = {有界モデル検査ツールを用いたC言語プログラム部分合成},
 volume = {2016},
 year = {2016}
}