近似手法と数式処理の融合による実数多項式制約の効率化

• 研究課題/領域番号: 23300005
• 研究種目: 基盤研究(B)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
• 研究分担者: 関 浩之 名古屋大学, 情報科学研究科, 教授 (80196948) ; 廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
• 研究協力者: ヴ シュアン ツング ; ト ヴァン カン
• 研究期間 (年度): 2011-04-01 – 2015-03-31
• 研究課題ステータス: 完了 (2014年度)
• 配分額: 20,150千円 (直接経費: 15,500千円、間接経費: 4,650千円); 2014年度: 4,940千円 (直接経費: 3,800千円、間接経費: 1,140千円); 2013年度: 4,940千円 (直接経費: 3,800千円、間接経費: 1,140千円); 2012年度: 4,940千円 (直接経費: 3,800千円、間接経費: 1,140千円); 2011年度: 5,330千円 (直接経費: 4,100千円、間接経費: 1,230千円)
• キーワード: ソフトウェア / 仕様記述 / 仕様検証 / 制約解消 / 数式処理 / SMTソルバ / 多項式制約 / 充足性判定

研究成果の概要

本研究では、多項式制約解消アルゴリズムである区間制約伝播の拡張としてraSAT ループを提案し、SMTソルバ raSATとして実装を行った。制約解消の解は SAT（充足可能）かUNSAT（充足不能）だが、SAT検出はエラー検出、UNSAT検出はループ不変式生成に用いられる。数百変数程度の大規模な問題に対し、実質的に後者が解けるのはUNSATコア（小さな部分制約で充足不能となるもの）を発見した場合に限られ、前者はすべての制約の充足性の確認が必要なため、実用上より困難である。本研究ではSAT検出に焦点をあて、SMTlibベンチマーク上の実験で答えが未知であった複数の問題のSATを検出した。

研究成果

• [雑誌論文] Deciding Schema k-Secrecy for XML Databases (2013)
  • 著者名/発表者名: Chittaphone Phonharath, Kenji Hashimoto, and Hiroyuki Seki
  • 雑誌名: IEICE Transactions on Information and Systems 巻: E96-D ページ: 1268-1277
  • NAID: 10031193987
  • 査読あり
• [雑誌論文] Node Query Preservation for Deterministic Linear Top-Down Tree Transducers (2013)
  • 著者名/発表者名: Kazuki Miyahara, Kenji Hashimoto, Hiroyuki Seki
  • 雑誌名: Electric Proceedings in Theoretical Computer Science 巻: 137 ページ: 27-37
  • DOI: 10.4204/eptcs.134.4
  • NAID: 130004841871
  • 査読あり
• [学会発表] raSAT: SMT for Polynomial Inequality（口頭発表） (2014)
  • 著者名/発表者名: To Van Khanh, Mizuhito Ogawa
  • 学会等名: 第12回SMTワークショップ(SMT 2014)
  • 発表場所: ウィーン、オーストリア
  • 年月日: 2014-07-17 – 2014-07-18
• [学会発表] Verification of the Security against Inference Attacks on XML Databases(査読付) (2012)
  • 著者名/発表者名: Chittaphone Phonharath, Kenji Hashimoto, Hiroyuki Seki
  • 学会等名: 1st International Workshop on Trends in Tree Automata and Tree Transducers (TTATT2012)
  • 発表場所: 名古屋大学(2012年6月2日)(採録・発表予定)
  • 年月日: 2012-06-02
• [学会発表] Confluence of Non-Left-Linear TRSs via Relative Termination (査読付) (2012)
  • 著者名/発表者名: Dominik Klein, Nao Hirokawa
  • 学会等名: 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR2012, Springer LNCS 7180, pp.258-273)
  • 発表場所: Universidad de Los Andes, Merida, Venezuela (2012年3月11日～15日)
  • 年月日: 2012-03-11
• [学会発表] Positive-noise Affine Interval Arithmetic(査読なし) (2011)
  • 著者名/発表者名: Do Thi Bich Nogc, Mizuhito Ogawa
  • 学会等名: 情報処理学会第86回プログラミング研究会
  • 発表場所: 神奈川近代文学館(2011年11月1日～2日)
  • 年月日: 2011-11-02
• [学会発表] Runtime Control of a Program based on Quantitative Information Flow
  • 著者名/発表者名: Bao Trung Chu, Kenji Hashimoto, and Hiroyuki Seki
  • 学会等名: IEICE SS2013-60
  • 発表場所: 愛知県 豊田中央研究所
• [学会発表] SMT for Polynomial Constraints on Real Numbers
  • 著者名/発表者名: To Van Khanh, Mizuhito Ogawa
  • 学会等名: Tools for Automatic Program Analysis (TAPAS 2012), Electrical Notes in Theoretical Computer Science, Vol.289, pp.27-40（査読付）
  • 発表場所: Douville, France
• [学会発表] Determinacy and Subsumption for Single-valued Bottom-up Tree Transducers
  • 著者名/発表者名: Kenji Hashimoto,Ryuta Sawada,Yasunori Ishihara,Hiroyuki Seki,Toru Fujiwara
  • 学会等名: 7th International Conference on Language and Automata Theory and Applications (LATA 2013), Springer LNCS 7810, pp.335-346（査読付）
  • 発表場所: Bilbao, Spain
• [学会発表] 決定性線形下降木変換器における頂点問合せ保存
  • 著者名/発表者名: 宮原 一喜, 橋本 健二, 関 浩之
  • 学会等名: 電子情報通信学会技術研究報告, SS2012-38, Vol.112, No.275, pp.13-18（査読なし）
  • 発表場所: 広島市立大学
• [学会発表] Determinacy and Subsumption of Single-valued Bottom-up Tree Transducers
  • 著者名/発表者名: Kenji Hashimoto, Ryuta Sawada, Yasunori Ishihara, Hiroyuki Seki, Toru Fujiwara
  • 学会等名: 第15回プログラミングおよびプログラミング言語ワークショップ（PPL 2013）, カテゴリ2（査読なし）
  • 発表場所: 会津若松市
• [備考] raSAT
  • URL: http://www.jaist.ac.jp/~mizuhito/tools/rasat.html
• [備考] SMT raSAT download
  • URL: http://www.jaist.ac.jp/~mizuhito/tools/rasat.html