ランキング関数の回帰推定による関数型言語の停止性検証

• Item type: Trans(1)
• 公開日: 2020-10-23
• タイトル: ランキング関数の回帰推定による関数型言語の停止性検証
• タイトル / 言語: en
• タイトル: Termination Verification for Functional Programs via Regression Prediction of Ranking Function
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要, Unrefereed Presentatin Abstract]
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 九州大学システム情報科学府
• 著者所属: 九州大学システム情報科学府
• 著者所属: 九州大学システム情報科学府
• 著者所属: 九州大学システム情報科学府
• 著者所属(英): en
• 著者所属(英): Graduate School and Faculty of Information Science and Electrical Engineering, Kyushu University
• 著者所属(英): en
• 著者所属(英): Graduate School and Faculty of Information Science and Electrical Engineering, Kyushu University
• 著者所属(英): en
• 著者所属(英): Graduate School and Faculty of Information Science and Electrical Engineering, Kyushu University
• 著者所属(英): en
• 著者所属(英): Graduate School and Faculty of Information Science and Electrical Engineering, Kyushu University
• 著者名: 村本, 大起; 佐藤, 亮介; 鵜林, 尚靖; 亀井, 靖高
• 著者名(英): Daiki, Muramoto; Ryosuke, Sato; Naoyasu, Ubayashi; Yasutaka, Kamei
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: プログラムの停止性検証は重要な研究課題の1つである．停止性検証を行う手法として，遷移不変条件となるランキング関数を推定するものが有力である．ここで，ランキング関数とはループまたは再帰ごとに値がつねに減少し，かつつねに正となる性質を持つ写像である．既存研究では，高階関数を含む関数型言語に対しSMTソルバを用いてランキング関数を推定し停止性検証を行っているが，末尾再帰関数のような制御フローに直接かかわらない引数を多く含むものに関しては正しい推定が難しく，簡単な書き換えによって検証できなくなるものが存在していた．本研究では，ランキング関数の推定方法に線形回帰を用いて，制御フローに関係のない引数を多く含むプログラムについてもなるべく検証ができるように改善を行う．提案する関数の停止性の検証手法は，まず仮のランキング関数を定める．そしてランキング関数が妥当であるかをチェックする．ランキング関数が妥当であれば検証成功．そうでない場合，得られた反例から引数の実際にとる値を取得する．得られた引数の値から新たなランキング関数を線形回帰で推定してランキング関数の妥当性検証へ戻り，妥当性検証が成功するまで繰り返し行う．また，本手法のプロトタイプとしてOCamlのサブセットを対象とした停止性検証器ツールを作成した．そして，ツールを用いて自動で検証できるものを調査した実験についても報告する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Termination verification is one of the important research topics. One way to verify the termination of a program is to infer a ranking function, which is monotonically decreasing and is always positive. An existing method for verifying termination of higher-order functional programs via inference of ranking functions has difficulty with accurate inference of ranking functions for programs whose arguments do not relate directly to its control flow like tail recursive functions, and there are some simple transformed programs cannot be verified by the method. In this presentation, we improve the existing method by using linear regression in order to verify such programs as much as possible. Our approach follows: set temporary ranking function, check if ranking function is valid, success verification if ranking function is valid. Otherwise, generate an assignment of the value to the variable from the obtained counterexample, infer ranking function via linear regression, and return to verification of ranking function. In this presentation, we implement the prototype of our method and show preliminary experiments.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 13, 号 4, p. 27-27, 発行日 2020-10-23
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会