有界モデル検査ツールを用いたC言語プログラム部分合成

• Item type: Symposium(1)
• 公開日: 2016-09-07
• タイトル: 有界モデル検査ツールを用いたC言語プログラム部分合成
• タイトル / 言語: en
• タイトル: Partial C-Program Synthesis on Bounded Model Checker
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 高位合成
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: 東京大学大学院工学系研究科電気系工学専攻
• 著者所属: 東京大学工学部電子情報工学科
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属(英): en
• 著者所属(英): Dept. of Electrical Engineering and Information Systems, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Dept. of Electrical Engineering and Information Systems, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center, The University of Tokyo
• 著者名: 木村, 悠介; 石山, 薫太郎; 藤田, 昌宏
• 著者名(英): Yusuke, Kimura; Kuntaro, Ishiyama; Masahiro, Fujita
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 従来から入出力の論理的使用からプログラムを合成する研究が進められてきている．これに対して最近，合成対象プログラムに対し，シンタックス上の制限を加えることで探索範囲を絞り，限られた数の入出力組のみで自動合成する手法が注目されている．比較的少数の入出力組からプログラムを合成できるので，仕様の詳細は不明だが処理内容の概要が分かっている場合などに適用できる．本研究ではこの従来手法を拡張し，テンプレートを利用した合成手法を提案する．当手法では，プログラム中の何カ所かの不明な部分に対して矛盾のない解を自動的に生成することができる．C 言語用の有界モデル検査ツールを利用した実装を利用して，数 100 行規模の暗号化プログラムや制御ソフトウェアを合成した結果について報告する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌情報: DAシンポジウム2016論文集; 巻 2016, 号 12, p. 62-67, 発行日 2016-09-07
• 出版者 / 言語: ja
• 出版者: 情報処理学会