| 研究課題/領域番号 |
23300005
|
|---|
| 研究種目 |
基盤研究(B)
|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
|
|---|
| 研究分担者 |
関 浩之 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80196948)
廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
|
|---|
| キーワード | ソフトウェア / 仕様記述 / 仕様検証 / 制約解消 / 数式処理 |
|---|
| 研究概要 |
実数多項式制約解消の効率化において、1.実数多項式不等式の制約を解くSMTの設計・実装(北陸先端大・小川)、2.数式処理に基づく実数多項式制約の厳密解を与えるQE-CADアルゴリズムの持ち上げ段階への書換え手法の応用の検討(北陸先端大・廣川)、3.量的情報流解析への応用の検討(奈良先端大・関)を進めた。
1.については、実用的な数式に適した区間演算の設計(情処プログラミング研究会発表)・比較を進め、現在、区間演算に基づく(オーヴァー)近似解析を背景理論とするSMTのプロトタイプの実装をminiSATをベースとして行った。さらにアルゴリズム・実装の双方の改良を進めている。
2.については、項書換え系の完備化手法をGroebner基底の計算への直接的な応用を検討したが、項書換え系における効率化のポイントとGroebner基底のポイントが異なることが判明し、現在、再検討を行っている。その検討の際、停止しない非線形項書換え系の合流性の新たな十分条件をbyproductとして発見した。(国際会議LPAR2012発表、2011年7月より博士課程学生を研究員雇用。)
3.については、連続値となる量的情報流の前段階として、離散値となる量的情報流として、XMLデータベーススキーマSのk-安全性について検討を行った。スキーマSの公開問合せを組み合せて、秘匿情報の候補値をk個未満に絞りこめないとき、Sはk-安全であるという。スキーマSのk-安全性が有限のkに対して判定不能であること、k=∞のとき判定可能であることを示した。(国際ワークショップTTATT2012発表。)
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
主たる理由は、北陸先端大側で、区間近似演算を用いたSMTの設計・実装が遅れたこと、Groebner基底の計算への項書換え系手法(完備化)の適用の目算が外れたためである。ただし、当初の予定外ではあるがbyproductとして、停止しない非線形項書換え系の合流性の新たな十分条件が得られた。(停止しない非線形項書換え系は、現在、項書換え系の分野で、もっともチャレンジングなトピックである。)
|
| 今後の研究の推進方策 |
当面は、(オーヴァー)近似区間演算を用いたSMTに(アンダー)近似としてのテスト手法を組合せ、相互に詳細化して、精度を得るアプローチを設計・実装を進め、さらに2013年のSMT competitionへの参加を目標とする。さらにツール自体の健全性を保証するために精度保証付数値計算の利用を検討する。
また量的情報流解析については、(連続値)情報流解析の実数多項式制約による定式化、さらに暗号アルゴリズムのサイドチャネル攻撃に対する耐性評価の応用の検討を進める。QE-CADアルゴリズムの効率化については、原点に戻り、anti-chainの手法の適用可能性を検討する。
|
