変数値域を限定した試行に基づく高次制約問題の充足可能性推定方法の検討

• Item type: Trans(1)
• 公開日: 2017-01-06
• タイトル: 変数値域を限定した試行に基づく高次制約問題の充足可能性推定方法の検討
• タイトル / 言語: en
• タイトル: Estimation of Satisfiability for High Order Constraint Problem Based on Trials with Range Restriction of Variabels
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要]
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 成蹊大学大学院理工学研究科
• 著者所属: 成蹊大学大学院理工学研究科
• 著者所属: 成蹊大学大学院理工学研究科
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Seikei University
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Seikei University
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Seikei University
• 著者名: 中山, 寛己; 高野, 保真; 千代, 英一郎
• 著者名(英): Hiroki, Nakayama; Yasunao, Takano; Eichiro, Chishiro
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 近年，SMTソルバの研究がさかんに行われてきており，様々な制約問題を解けるよう飛躍的に進歩している．しかしながら，SMTソルバは線形制約式の解を短時間で求められることが多いのに対し，高次の制約式の解を求めるのに時間がかかってしまうことがある．たとえば，代表的なプログラム検査であるループ停止性検査等で必要となる複雑な制約式の場合，検査に数日を要することもあり，実用上の課題となっている．この問題に対して，本発表では，変数のとりうる値域を限定した検査を，値域を変えて繰り返すことで，制約式の充足可能性を推定する方法について報告する．それぞれの試行を短い時間で打ち切ることにより，結果が得られないことを避けることができる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In recent years, studies of SMT solvers are conducted flourishingly and progress drastically to be able to solve various constraint satisfaction problems. However, while the SMT solver tends to find solution of linear constraints efficiently, it may take a few days to find solutions of the higher degree constraints needed for checking loop termination. For this problem, we examine methods to estimate the satisfiability of constraints by iterative checking (trial) with range restriction of variables. In this presentation, we report some experimental results about trial.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 10, 号 1, p. 34-34, 発行日 2017-01-06
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会