メニュー
検索
研究課題をさがす
研究者をさがす
KAKENの使い方
日本語
英語
全文検索
詳細検索
絞り込み条件
絞り込み
研究期間 (開始年度)
-
検索結果: 24件 / 研究者番号: 80196948
1
2
›
Next
»
End
すべて選択
ページ内選択
XMLで出力
テキスト(CSV)で出力
表示件数:
20
50
100
200
500
適合度
研究開始年: 新しい順
研究開始年: 古い順
配分額合計: 多い順
配分額合計: 少ない順
1.
データハイブリッドなリアクティブプログラムの解析技術と自動合成・説明抽出への応用
研究課題
研究種目
基盤研究(B)
審査区分
小区分60050:ソフトウェア関連
研究機関
名古屋大学
研究代表者
関 浩之
名古屋大学, 情報学研究科, 教授
研究期間 (年度)
2022-04-01 – 2025-03-31
交付
キーワード
計算論的ゲーム構造
/
プログラム自動合成
/
プライバシー保護
/
形式言語理論
/
レジスタ計算モデル
/
プログラム自動生成
/
重み付き計算モデル
研究開始時の研究の概要
組込み制御ソフトウェアに代表されるリアクティブプログラムの信頼性を担保するための数理的手法を実用システムに適用可能にするためには,データ値,時間,確率等の量的概念を考慮した計算モデルの設定が鍵となる.本研究ではこのような問題意識のもとに,以下の課題に取り組む.
2.
データと時間を扱うオートマトンネットワークの合成的アクティブ学習に基づく設計手法
研究課題
研究種目
基盤研究(B)
審査区分
小区分60050:ソフトウェア関連
研究機関
名古屋大学
研究代表者
結縁 祥治
名古屋大学, 情報学研究科, 教授
研究期間 (年度)
2021-04-01 – 2026-03-31
交付
キーワード
アクティブ学習
/
頑健性
/
Assume-Gurantee検証
/
拡張有限状態オートマトン
/
並行計算モデル
/
イベントクロックオートマトン
/
アクティブ学習アルゴリズム
/
分割検証
/
Assume-Gurantee
/
SMTソルバー
/
到達可能性解析
研究開始時の研究の概要
実データを含むサブシステムの振舞いを拡張有限状態機械(EFSM)としてモデル化し振舞い合成と分解について、通信プロセスの形式化に基づい て振舞いの頑健性として振舞いの安定性を導く設計手法を確立する。この研究においては、システムの分解と合成の検証における抽象モデルと 実現モデルとの関係に着目して研究を
...
研究実績の概要
本年度は,時間経過モデルに対して可逆計算の概念を導入したモデルについても検討を開始した.時間経過モデルは,複数のコンポーネントが同期をする際に通信を行わず,互いに持つクロックの差分によって同期を可能にする.しかし,設計の際に時間経過による同期が想定した組み合わせにならない場合は,デッドロックや予定外
...
現在までの達成度 (区分)
2: おおむね順調に進展している
この課題の研究成果物
国際共同研究 (1件) 雑誌論文 (7件 うち国際共著 3件、査読あり 7件、オープンアクセス 3件) 学会発表 (4件 うち国際学会 2件)
3.
数理論理手法と人工知能手法の融合に基づくマルウェアの自動意味理解
研究課題
研究種目
挑戦的研究(開拓)
審査区分
中区分60:情報科学、情報工学およびその関連分野
研究機関
北陸先端科学技術大学院大学
研究代表者
小川 瑞史
北陸先端科学技術大学院大学, 先端科学技術研究科, 教授
研究期間 (年度)
2020-07-30 – 2026-03-31
交付
キーワード
動的記号実行
/
命令セット
/
バイナリコード
/
マルウェア
/
自然言語処理
/
マルウェア解析
/
記号実行
/
API
/
ネィティブコード
/
マルウェア意味解析
/
形式的意味自動抽出
/
形式仕様自動抽出
/
深層学習
研究開始時の研究の概要
人間には解釈困難なバイナリコードに対し(1)操作的意味はレジスタ・フラッグ・メモリ・スタック上の状態遷移系として定義可能、(2)各命令仕様はリジッドな自然言語記述、(3)エミュレータ等テスト環境が完備などの観察に立脚し、英文マニュアルから命令の操作的意味自動抽出によりBE-PUM(x86), Cor
...
研究実績の概要
R4年度は、主にARM/Androidを対象とした動的記号実行器Coranaの拡張Corana-Xの実装・開発を進めた。Androidマルウェアは主にApkファイル形式であり、Javaに準ずる記述に加え native code (ARM, x86等)やLinuxライブラリ関数呼出しを含むため、実行が
...
現在までの達成度 (区分)
2: おおむね順調に進展している
この課題の研究成果物
雑誌論文 (3件 うち国際共著 1件、査読あり 3件、オープンアクセス 1件) 学会発表 (8件 うち国際学会 5件) 備考 (2件)
4.
ソフトウェアモデルへの量的尺度の導入とプログラム解析への応用
研究課題
研究種目
基盤研究(B)
審査区分
小区分60050:ソフトウェア関連
研究機関
名古屋大学
研究代表者
関 浩之
名古屋大学, 情報学研究科, 教授
研究期間 (年度)
2019-04-01 – 2023-03-31
完了
キーワード
ソフトウェア検証
/
モデル検査
/
プログラム自動合成
/
レジスタオートマトン
/
形式言語理論
/
量的情報流
/
線形時相論理
/
セキュリティ
/
ゲーム構造
/
アクティブ学習
/
重み付き文脈自由文法
/
mu-計算
/
プログラム合成
/
XML
研究開始時の研究の概要
ソフトウェアの信頼性を担保するための数理的解析・検証技術を実用システムに適用可能にするためには,対象とする系をデータ値,時間,確率,情報量等の量的概念を考慮した数理的モデルに拡張する必要がある.本研究ではこのような問題意識のもとに,量的情報流の動的解析,データ値をもつ計算モデルとその構造化文書処理へ
...
研究成果の概要
ソフトウェアの信頼性を保証する手法として,量的情報流の動的解析,データ値を扱う計算モデル,重み付き計算モデルの3つの課題について研究を行った.動的情報流の2つの定義を提案し,その計算量解析を行うとともに,モデル計数ツールを用いた実装を行った.レジスタ計算モデルについて,レジスタ付きCFGの基本問題の
...
この課題の研究成果物
雑誌論文 (12件 うち国際共著 1件、査読あり 12件、オープンアクセス 6件) 学会発表 (12件)
5.
実時間性を持つ並行プログラムに対するデバッグのための逆方向計算モデル
研究課題
研究種目
基盤研究(B)
研究分野
ソフトウェア
研究機関
名古屋大学
研究代表者
結縁 祥治
名古屋大学, 情報学研究科, 教授
研究期間 (年度)
2017-04-01 – 2021-03-31
完了
キーワード
可逆計算
/
並行計算モデル
/
並行プログラム
/
可逆実行環境
/
可逆デバッガ
/
可逆計算実行環境
/
可逆抽象機械
/
逆方向デバッグ技法
/
逆方向計算
/
実時間プログラム
/
通信プロセス計算
/
プログラミング言語
/
通信プロセスモデル
/
逆計算モデル
/
バックトラック逆計算
/
構造操作意味規則
/
因果無矛盾性
/
並行計算
/
デバッグモデル
/
離散時間モデル
/
並行プログラミング言語
/
計算モデル
/
実時間性
/
ソフトウエア学
/
ソフトウェアデバッグ
/
逆計算
研究成果の概要
本研究の目的は、並行性をもつソフトウェアにおいて、逆計算のメカニズムを応用して新たな解析手法を与えることである。近年の並行性を持つソフトウェアの振舞いにおいては、同時に実行されるプログラムの振舞いは非決定的であり、どのように相互作用を行ったかということを逆にたどることはプログラムの動的解析にとって非
...
この課題の研究成果物
国際共同研究 (5件) 雑誌論文 (21件 うち国際共著 12件、査読あり 21件、オープンアクセス 15件) 学会発表 (6件 うち国際学会 2件)
6.
ソフトウェアセキュリティ・プライバシーのための静的解析・動的検査法
研究課題
研究種目
基盤研究(B)
研究分野
ソフトウェア
研究機関
名古屋大学
研究代表者
関 浩之
名古屋大学, 情報学研究科, 教授
研究期間 (年度)
2015-04-01 – 2019-03-31
完了
キーワード
セキュリティ
/
木オートマトン
/
木変換器
/
文法圧縮
/
マルウェア解析
/
SMTソルバ
/
レジスタオートマトン
/
レジスタ文脈自由文法
/
計算複雑さ
/
プログラムセキュリティ
/
動的情報漏洩量
/
ソフトウェア解析
/
プライバシー
/
形式言語理論
/
自動解析
/
XML
/
圧縮
/
木文法
/
トップ木
/
文脈自由文法
/
有向グラフ
/
情報保存性
/
直線的文脈木文法
/
XPath
研究成果の概要
非決定性木変換器における問合せ保存性について考察した.木文法およびトップ木に基づく圧縮法,圧縮データを解凍することなく直接問合せおよび更新する手法を提案・実装した.文脈自由文法にデータ値を扱う能力を限定的に加えたレジスタ文脈自由文法(RCFG)について,所属問題と空問題の計算量がEXPTIME完全で
...
この課題の研究成果物
雑誌論文 (2件 うち査読あり 2件、謝辞記載あり 1件) 学会発表 (21件 うち国際学会 5件)
7.
ソフトウェアセキュリティのための量を扱う計算モデルの提案
研究課題
研究種目
挑戦的萌芽研究
研究分野
ソフトウェア
研究機関
名古屋大学
研究代表者
関 浩之
名古屋大学, 情報学研究科, 教授
研究期間 (年度)
2014-04-01 – 2018-03-31
完了
キーワード
セキュリティ
/
量的情報流
/
k-安全性
/
XMLデータベース
/
時間攻撃
/
差分プライバシー
/
SMT
/
SAT
/
プライバシー
/
データベース
/
隠れマルコフモデル
/
タイミング攻撃
/
情報理論
研究成果の概要
ソフトウェアのセキュリティやプライバシーの尺度として,量的情報流,差分プライバシー等が提案され種々議論されている.本研究課題では主に量的情報流を中心にいくつかの定量的尺度について,それを計算するアルゴリズムや,そのような尺度に基づくソフトウェアの安全性検証手法の開発に取り組んだ.具体的に,復号アルゴ
...
この課題の研究成果物
雑誌論文 (1件 うち査読あり 1件) 学会発表 (10件 うち招待講演 1件)
8.
機械学習と最適化に基づく RNA タンパク質相互作用予測
研究課題
研究種目
挑戦的萌芽研究
研究分野
生体生命情報学
研究機関
奈良先端科学技術大学院大学
研究代表者
関 浩之
奈良先端科学技術大学院大学, 情報科学研究科, 教授
研究期間 (年度)
2011 – 2012
完了
キーワード
バイオインフォマティクス
/
RNA-タンパク質相互作用
/
RNA2次構造
/
RNA間相互作用
/
RNA構造アラインメント
/
機械学習
/
最適化
/
RNA2次構造
研究概要
本研究ではRNA配列情報解析の視点から、まず、単一RNA塩基配列が与えられた時の複雑な折り畳み構造を予測する数理的手法を開発した。次に、複数の配列が与えられた場合に、配列間の対応付けと各構造を同時に予測する手法の開発も行った。これら開発手法について実際の生物データを用いて予測性能評価を行い、既存手法
...
この課題の研究成果物
雑誌論文 (8件 うち査読あり 8件) 学会発表 (28件) 図書 (2件) 備考 (2件)
9.
形式言語理論に基づく静的解析法とその安全性検査への応用
研究課題
研究種目
基盤研究(B)
研究分野
ソフトウエア
研究機関
名古屋大学
(2012-2015)
奈良先端科学技術大学院大学
(2011)
研究代表者
関 浩之
名古屋大学, 情報科学研究科, 教授
研究期間 (年度)
2011-04-01 – 2016-03-31
完了
キーワード
ソフトウェア検証
/
形式言語理論
/
モデル検査
/
XML
/
情報保存性
/
木変換器
/
セキュリティ
/
木オートマトン
/
圧縮
/
頂点問合せ
/
木文法
研究成果の概要
木言語理論を用い,XML文書等の構造化データに対する情報保存性およびセキュリティに関して以下の成果を挙げた.変換vが問合せqを保存するとは、任意のデータtに対して, tへの問合せqの結果を,変換の結果v(t)からも得ることができることをいう.木変換器や頂点問合せ等のモデルに基づき問合せ保存性問題の判
...
この課題の研究成果物
雑誌論文 (3件 うち査読あり 3件) 学会発表 (10件 うち国際学会 1件、招待講演 1件)
10.
近似手法と数式処理の融合による実数多項式制約の効率化
研究課題
研究種目
基盤研究(B)
研究分野
ソフトウエア
研究機関
北陸先端科学技術大学院大学
研究代表者
小川 瑞史
北陸先端科学技術大学院大学, 情報科学研究科, 教授
研究期間 (年度)
2011-04-01 – 2015-03-31
完了
キーワード
ソフトウェア
/
仕様記述
/
仕様検証
/
制約解消
/
数式処理
/
SMTソルバ
/
多項式制約
/
充足性判定
研究成果の概要
本研究では、多項式制約解消アルゴリズムである区間制約伝播の拡張としてraSAT ループを提案し、SMTソルバ raSATとして実装を行った。制約解消の解は SAT(充足可能)かUNSAT(充足不能)だが、SAT検出はエラー検出、UNSAT検出はループ不変式生成に用いられる。数百変数程度の大規模な問題
...
この課題の研究成果物
雑誌論文 (2件 うち査読あり 2件) 学会発表 (9件) 備考 (2件)
11.
言語組込みアクセス制御の高信頼化に関する研究
研究課題
研究種目
基盤研究(C)
研究分野
ソフトウエア
研究機関
奈良先端科学技術大学院大学
研究代表者
関 浩之
奈良先端科学技術大学院大学, 情報科学研究科, 教授
研究期間 (年度)
2008 – 2010
完了
キーワード
アクセス制御
/
情報流解析
/
セキュリティ
/
実行履歴
/
スタック検査
/
自動生成
/
静的解析
/
情報流解
研究概要
本研究ではまず,再帰プログラムPとセキュリティ仕様Sが与えられたとき,Sを満たすようにPにアクセス権検査文を埋め込む自動生成問題を定義した.そして,自動生成問題がco-NP困難であることを示した.次に,プッシュダウンシステム(PDS)モデル検査法を利用して自動生成問題を解くアルゴリズムを提案した.さ
...
この課題の研究成果物
雑誌論文 (5件 うち査読あり 4件) 学会発表 (22件)
12.
無限状態モデル検査を用いた高信頼性ソフトウェアの自動検証に関する研究
研究課題
研究種目
基盤研究(C)
研究分野
ソフトウエア
研究機関
奈良先端科学技術大学院大学
研究代表者
関 浩之
奈良先端科学技術大学院大学, 情報科学研究科, 教授
研究期間 (年度)
2006 – 2007
完了
キーワード
形式的検証
/
モデル検査
/
静的解析
/
形式言語
/
アクセス制御
/
セキュリティ
/
実行履歴
/
XML
/
ソフトウェア学
研究概要
(1)再帰的プログラムのモデル検査法:実行履歴に基づくアクセス制御付きプログラム(HBACプログラム)の安全性検証法において、種々の最適化を行うことにより、高速検証が行えることを実証した。提案手法ではモデル検査問題を文脈自由文法(CFG)の空判定問題に帰着しており、アクセス権の個数に対して指数的な検
...
この課題の研究成果物
雑誌論文 (21件 うち査読あり 10件) 学会発表 (14件)
13.
アクティブソフトウェアの設計検証手法に関する研究
研究課題
研究種目
基盤研究(C)
研究分野
ソフトウエア
研究機関
奈良先端科学技術大学院大学
研究代表者
関 浩之
奈良先端科学技術大学院大学, 情報科学研究科, 教授
研究期間 (年度)
2004 – 2005
完了
キーワード
形式的検証
/
モデル検査
/
アクティブソフトウェア
/
アクセス制御
/
静的解析
/
実行履歴
/
形式言語
/
セキュリティポリシー
研究概要
(1)実行履歴に基づくアクセス制御系の検証法:Abadiらのアクセス制御法を包摂するHBAC(History-Based Access Control)プログラムという形式モデルを提案した.次に,HBACモデルに対して安全性検証問題を定義し,この検証問題が一般には決定性指数時間完全であること,アクセ
...
この課題の研究成果物
雑誌論文 (23件)
14.
動的アクセス制御を行なうソフトウェアのセキュリティ検証に関する研究
研究課題
研究種目
基盤研究(C)
研究分野
計算機科学
研究機関
奈良先端科学技術大学院大学
研究代表者
関 浩之
奈良先端科学技術大学院大学, 情報科学研究科, 教授
研究期間 (年度)
2002 – 2003
完了
キーワード
アクセス制御
/
セキュリティ
/
安全性
/
検証
/
モデル検査
/
ポリシー
研究概要
アクセス制御におけるポリシーとは,「誰が、どのデータに対して、どのような操作を行なうことを許可/禁止するか、または義務であるか」を記述したものをいう。本研究ではまず、以下の特長をもつポリシー記述言語を設計した。
...
この課題の研究成果物
文献書誌 (23件)
15.
ユーザタスクの形式的記述に基づくインタラクティブシステム設計法
研究課題
研究種目
基盤研究(C)
研究分野
計算機科学
研究機関
奈良先端科学技術大学院大学
研究代表者
関 浩之
奈良先端科学技術大学院大学, 情報科学研究科, 教授
研究期間 (年度)
2000 – 2001
完了
キーワード
ユーザインタフェース
/
インタラクティブシステム
/
形式的検証
/
プロトタイプ自動生成
/
タスク図
/
代数的仕様
/
抽象的順序機械
/
ソフトウェア設計法
研究概要
1.タスク図を用いたインタラクティブシステム設計法について,以下の研究を行った.
...
この課題の研究成果物
文献書誌 (13件)
16.
文書データベースにおける演繹的問合せ言語の設計
研究課題
研究種目
奨励研究(A)
研究分野
計算機科学
研究機関
奈良先端科学技術大学院大学
研究代表者
関 浩之
奈良先端科学技術大学院大学, 情報科学研究科, 教授
研究期間 (年度)
1997 – 1998
完了
キーワード
文書データベース
/
情報検索
/
カテゴリ構造
/
World Wide Web
/
データベース
/
系列データモデル
/
論理型言語
/
ホーン節
/
問合せ言語
研究概要
本研究2年目においては,1年目に検討した文書検索/問合せ支援方式を洗練し,検索支援システムを試作した.WWWに代表される大規模文書データを検索するサービスとして,キーワード検索とディレクトリサービスが提供されている.しかし,前者ではユーザの意図する検索結果を得るのに必要な検索式を考えるのが難しい.ま
...
この課題の研究成果物
文献書誌 (5件)
17.
オブジェクト指向データベースプログラムの型検査法とアクセス制御への応用
研究課題
研究種目
奨励研究(A)
研究分野
計算機科学
研究機関
奈良先端科学技術大学院大学
研究代表者
関 浩之
奈良先端科学技術大学院大学, 情報科学研究科, 助教授
研究期間 (年度)
1995
完了
キーワード
オブジェクト指向データベース
/
型検査
/
アクセス制御
/
アクセス権
/
計算複雑さ
研究概要
1.オブジェクト指向データベースのモデルとして、Hullらの更新スキーマを採用した。更新スキーマSとデータベースインスタンスIが与えられたとき、S内の任意のメソッドの実行中に結合すべきメソッドが一意に定まるとき、インスタンスIはSのもとで型整合性をもつという。本研究では、与えられた再帰なし更新スキー
...
この課題の研究成果物
文献書誌 (4件)
18.
制約指向型形式文法に対する構文解析法に関する研究
研究課題
研究種目
奨励研究(A)
研究分野
計算機科学
研究機関
奈良先端科学技術大学院大学
研究代表者
関 浩之
奈良先端科学技術大学院大学, 情報科学研究科, 助教授
研究期間 (年度)
1994
完了
キーワード
形式文法
/
形式言語
/
構文解析
/
オートマトン
/
木オートマトン
研究概要
制約指向文法の構文解析法を考察するため、この種の文法で定義される言語のクラスを特徴付ける受理機のクラスとして、木記憶をもつ木オートマトン(TTA)を提案した.
この課題の研究成果物
文献書誌 (1件)
19.
自然言語で書かれたソフトウェア仕様書解析のための統合環境の開発
研究課題
研究種目
奨励研究(A)
研究分野
計算機科学
研究機関
大阪大学
研究代表者
関 浩之
大阪大学, 基礎工学部, 助教授
研究期間 (年度)
1993
完了
キーワード
代数的仕様
/
構文解析
/
自然言語
/
形式文法
/
構文規則
/
順序機械
/
通信プロトコル
/
ソフトウェア工学
研究概要
自然言語で書かれたソフトウェア仕様書解析のための統合環境に関する研究を行い,以下の成果を得た.
この課題の研究成果物
文献書誌 (4件)
20.
会計知識の代数的仕様記述と専門家システム構築に関する研究
研究課題
研究種目
一般研究(C)
研究分野
情報学
研究機関
滋賀大学
研究代表者
森 將豪
滋賀大学, 経済学部, 教授
研究期間 (年度)
1991
完了
キーワード
代数的仕様記述
/
会計原則
/
エキスパ-トシステム
研究概要
上記の研究課題に関して得られた知見を以下に述べる。
この課題の研究成果物
文献書誌 (1件)
1
2
›
Next
»
End