修士論文一覧
酒井研（酒井・西田研）修了生
- 伊藤 健太、
時系列CDCL と対称成分キャッシングを利用した成分分割型投射モデル計数の形式化とソルバ実装
- 佐藤 宏志、
指移動の時間的ゆとりの概念を導入したピアノ運指推定
- 蘇 日娜（ソリナ）、
Execution-Result Analyzer for Debugging Problem Descriptions of SQL-Based Combinatorial Optimization
酒井・西田研修了生
- 天春 陽介、
ピアノ演奏の未量子化MIDIデータに対する声部分割の最適化問題への帰着
- 小栗 滉介、
グラフパスとペントミノパズル解の計数のための問題分割型アルゴリズム
- 平等 望、
制約付き書換え帰納法における等式の場合分け分割の推論保存性
- 中村 翔平、
投射モデル計数におけるソルバ選択のための実行時間予測
- 松見 歩佳、
分離論理制約付き項書換え系の提案とポインタを伴うプログラムのモデル化
酒井研修了生
- 葉 翔太、
成分分割型投射モデル計数における論理式のグラフ表現を用いた変数選択ヒューリスティックス
- 山内 啓輔、
項書換え系の書換え帰納法における並列推論とそのダイヤモンド性の十分条件
- 赤尾 健太、
単旋律音楽における休符付きリズムの自動採譜のための確率付き文法の構成法と評価法
- 加藤 拓洋、
意味論規則の具体化によるLLVM中間表現から論理制約付き項書換え系への変換
- 小嶋 美咲、
制約付き書換えの全パス到達可能性への帰着による排他制御付きプログラムの実行時エラー検証
- 張 淑珺、
Study of Transformations between Cut-Free Cyclic Proofs and Rewriting-Induction Proofs
- 磯貝 孝明、
投射モデル列挙を目的とする簡約と変数順序を用いた効率的なBDD構築法
- 岸 潤一郎、
擬ブール制約の導入による組合せ最適化ソルバCombSQL+の高速化
- Donghoon Shin、
Proving Termination of Bit Vector Logically Constrained Term Rewrite Systems by Extracting Inner Loops in Dependency Graphs
- 比嘉 慎哉、
制約付き書換え帰納法におけるラグランジュ補間による補題生成
- 何 家琦、
Simplification of ROBDDs Using Equality of Variables
- 田端 浩明、
マクロ森変換器がXMLスキーママッピングの実現であることの決定手続き
- 西江 一志、
未定係数と存在限量子を含む等式を証明するための書換え帰納法の拡張
- 金澤 慶明、
論理制約付き項書換え系による大域変数とユーザ定義型を含むCプログラムのモデル化
- 坂梨 元軌、
組合せ最適化問題のためのSQLの拡張とSMTソルバを用いた実現
- 前田 侑也、
条件付き項書換え系の解析のためのナローイング計算木のベーシックナローイングへの拡張
- 笹野 智裕、
制約付き書換えにおける単調増加列への多項式解釈に基づく停止性証明
- 對馬 渓人、
被消去変数の整数解を保存する等式除去による線形整数制約ソルバの高速化
- 長江 悠太郎、
Finite Representations of Search Spaces for Existential Parameterised Boolean Equation Systems
- 中山 亮太、
A Reduction-Reflecting Structure-Preserving Transformation for Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems
- 水谷 慎之介、
ホーア論理の証明木から書換え帰納法の推論列への変換
酒井研・関研修了生
- 安藤 聡志、
OSS開発におけるパッチの特徴量を用いたコードレビュー結果の予測法
- 石月 清香、
Characterization and a decidable sufficient condition for confluenceof innermost terminating rewrite systems
- 石原 鷹、
制限付複製を含むトップダウン木変換器における問合せ保存性の決定可能な十分条件
- 黒田 貴之、
十分完全性を持たない階層的条件付き項書換え系の完備性証明
- 河邉 翔平、
Malbolgeプログラムを生成するための中間言語とそのコンパイラ
- 鈴木 涼介、
前処理とバックジャンプに基づく成分分割付き投射モデル計数の高速化
- 高山 隆之介、
木文法に基づき圧縮されたXML文書に対するデータ値を考慮した直接更新法
- 長尾 貴浩、
A rewriting induction framework for constrained inequalities
- 中島 聖斗、
量的情報流解析のためのモデル計数の高速化
- 浅井 孝俊、
XMLデータベースにおける木問合せのk-安全性のためのモデル計数を用いた検査法
- 内田 佑作、
組合わせ最適化問題のためのSQL言語の拡張とその実現
- 太田 浩一、
条件付き依存対法に基づく関数型プログラムの停止性証明のための項の到達不能性の十分条件
- 川本 佳史、
制約付き項書換え系における停止性と帰納的定理の同時証明法
- 後藤 健志、
木文法に基づくXML圧縮文書に対する更新手法
- 塚本 尚秀、
基数制約節の直接処理に基づくSATソルバの拡張法
- 中村 陽介、
ビルディングパズルの最小ヒント数について
- 柳澤 真志、
拡張Farkas補題の部分適用による非線形ループ不変式生成を用いたプログラム検証
坂部研・酒井研修了生
- 上山 智也、
制約付き項書換え系におけるナローイングの導入による停止性証明法の改良
- 尾前 貴則、
項書換え系の停止性証明のための重み付き経路順序の抽象化
- 片岡 巧、
部分関数を利用して定義された関数の等価性検証のための書換え帰納法
- 加藤 起騎、
難解言語Malbolgeの低級アセンブリ言語における条件分岐の記述と高級アセンブリプログラミング環境の構築
- 加藤 友郁、
条件付き項書換え系における逆Unfold問題とその発見的解法
- 栗木 隆太朗、
制約付き項書換えにおける関数合成の可換性の証明法
- 永塚 尚紀、
Size complexity of BDD constructed from Pseudo-Boolean constraints in mixed-radix base form
- 神谷 尚史、
単純型付き項書換え系における帰納的定理自動証明の戦略の提案
- 坂井 利光 、
シャローな等式集合の語問題への合同閉包アルゴリズムの適用法に関する研究
- 中野 靖大 、
制約付き木オートマトンの状態簡約化
- 東野 惇一郎、
配列を含むプログラムのための条件付き不等式形式のループ不変式の生成
- 松原 穂波、
単純型付き項上の高階辞書式経路順序へのカリー化の組み込み
- 杢谷 孔皓、
プログラム中の分離論理表明式に対する動的検査システムの開発
- 安藤 聡、
難解言語Malbolgeのプログラム作成のための中間言語の拡張と開発支援
- 大井 一展、
高階書換え系における静的依存対法の改良と引数切り落とし関数の下での実効規則
- 倉田 佳佑、
単純型付き項書換え系の停止性証明におけるカリー化の利用
- 柴 暢、
A Bounded-Integer Linear Solver based on Global Polynomial Watchdog Method
- 丁 維龍、
関数等価性を保証する木準同型写像の存在性を判定するためのSMTソルバの利用
- 丹羽 南、
On Determinization of Grammar Programs for Program Inversion
- 伏見 政晃、
プレスブルガー算術式の整数解を導出するための限量子除去アルゴリズムと単体法の逐次合成
- 尾関 朗、
単純型付き項書換え系における書換え帰納法について
- 朱 方彦、
順序制約を付加した論理式の充足可能性判定について
- 鈴木 英一、
関数呼び出しを持つプログラムの非線形ループ不変式の自動生成
- 高桑 一也、
関数等価性検証のための制約付き項書換え系の単純化
- 谷村 直樹、
単純型付き項書換え系における可触性に基つ?く高階経路順序の設計
- 服部 達哉、
On decidability of termination of term rewriting systems classified by
linearity and shallowness
- 日野 善信、
基本対称節を持つCNFの充足可能性判定におけるリテラル最小監視法について
- 松田 紘幸、
書換え帰納法に基つ?く高階定理自動証明器のための戦略に関する研究
- 岡田 大、
アクセス制御付き抽象データ型とその非干渉性
- 河野 証昭、
単純型付き項書換え系の停止性自動証明器の開発
- 倉橋 克尚、
制約付き木オートマトンの制約完全化と閉包性
- 鈴木 翔、
Argument Filterings and Usable Rules in Higher-Order Rewrite Systems
- 長坂 哲、
難解言語Malbolgeの弱チューリング完全性とプログラミング環境
- 馬場 達也、
等式理論を法とする充足可能性を判定するDPLL遷移系の設計と実装
- 大平 崇博、
次世代車載LANプロトコルにおける見逃し誤りの解析
- 小島 芳治、
Decidability of Context-Sensitive Innermost Reachability for Linear
Right-Shallow Term Rewriting Systems
- 小林 弘昌、
項書換え系の型付けに基づく停止性判定法の研究
- 中林 直生、
制約付き項書換え系の書換え帰納法における補題等式の自動生成
- 馬場 正貴、
例外処理を持つ関数型プログラムの停止性判定の研究
- 御宿 義勝、
右線形右シャローな項書換え系における文脈依存停止性の決定可能性について
- 伊藤 寛之、
効率的なパズル解法のための充足可能性問題への変換手法
- 鵜飼 謙児、
ビットエラー環境下における次世代車載LANプロトコルの動作解析
- 内山 敬太、
Decidability of Termination, Innermost Termination and Context-Sensitive Termination Properties for Term Rewriting Systems
- 馬野 洋平、
充足可能性判定ツールの基本対称関数導入による高速化と応用
- 坂田 翼、
制約付き項書換え系に対する書換え帰納法に関する研究
- 磯谷 泰巨、
強計算性に基づく静的依存対法による高階書換え系の停止性証明に関する研究
- 近藤 悟、
等式仕様の変換に基づくプログラム生成系GeneSysに関する研究
- 笹田 悠司、
等式付き書換えを用いた潜在帰納法とその振舞等価性自動証明への応用
- 水谷 知博、
導出過程の解析による論理プログラムの非停止性証明法
- 水野 清貴、
等式を規則化する変換の停止性に関する研究
- 村田 俊樹、
条件付き項書換え系における到達可能性に関する研究
- 山田 晃久、
An extension of soft typing for static detection of runtime type errors
- 王 誼、
Confluence of Length Preserving String Rewriting Systems is Undecidable
- 蒲田 明憲、
定理自動証明系HOPSYSの開発と高階プログラム検証への応用
- 黒川 翔、
情報流解析を用いたオブジェクト指向プログラムの安全性解析
- 櫻井 敬大、
ラベル付けを用いた単純型項書換え系の停止性証明法
- 古市 祐樹、
書換え理論に基づく手続き型プログラムの等価性検証に関する研究
- 三浦 浩一、
アンビエント計算の検証のための項書換え系への変換法の研究
- 飯澤 恒、
難解言語Malbolgeに基づくプログラム難読化に関する研究
- 岩田 篤史、
重なりを持つ項書換え系の正規化戦略に関する研究
- 王 易、
Some Classes of Term Rewriting Systems for which Termination is Decidable
- 奥谷 大介、
カラーペトリネットを用いた暗号プロトコルの機密性検証
- 佐伯 昌樹、
JoinJavaのプロセス移動と通信エラーに関する研究
- 田代 善彦、
Spi計算における機密性検証に関する研究
- 岡本 晃治、
最内戦略に基づく項書換え計算の効率化に関する研究
- 高須 洋平、
配列を用いた非線形再帰プログラムからの再帰除去
- 蛸島 洋明、
項書換え系への変換に基づくメタ項書き換え計算の停止性
- 松岡 武士、
プログラム最適化のための効率的なモデル検査手法
- 村田 龍彦、
項書換え系において到達可能性を判定する木オートマトンの生成に関する研究
坂部研修了生
- 岡田 泰典、
関数の暗号化に基づく耐タンパーモバイルエージェント
- 金子 伸幸、
ビジネスオブジェクトを利用したコンポーネント管理に基づく設計支援
- 田村 亮、
複製演算とAC演算を持つ系の単一化問題の解法
- 長島 正憲、
限量子付き等式仕様の変換に基づくプログラム生成に関する研究
- 山本 友和、
潜在帰納法に基づく振舞等価性の自動証明法
- 加治 洋丞、
帰納的完備化手続きに基づく定理証明の自動化に関する研究
- 佐野 嘉則、
項書換え系と木オートマトンを用いたセキュリティプロトコルの検証法における近似関数に関する研究
- 西尾 慎太郎、
文脈依存性を考慮した戦略とその項書換え系コンパイラへの応用
- 堀江 美保子、
再帰型をもつオブジェクト算法における例外処理の型システムに関する研究
- 吉仲 晃一、
Join算法とJAVAの融合言語JoinJAVAにおける同期通信機能に関する研究
- 加納 康資、
振舞等価性の自動証明のための潜在帰納法
- 木崎 真一郎、
アンビエント計算のプロセス方程式の解法に関する研究
- 鈴木 剛、
優先順序付き項書換え系の頭必須戦略の決定可能性
- 中村 敏広、
関数型言語における合成関数計算の効率化に関する研究
- 侭田 佳幸、
モデル検査オートマトンからの証明生成のモジュラー性に関する研究
- 西田 直樹、
Study on Inversion of Term Rewriting Systems
- 酒井 大介、
MLの型推論に基づくJoin算法の型推論システムの構築
- 冨田 泰弘、
代入が制約されたR単一化判定アルゴリズムに基づくR単一化子の発見法とその実現
- 洪 順姫、
メタ項書換え計算の合流性に関する研究
- 尾関 嘉一郎、
Join算法による並行計算の簡潔な記述が可能なJAVA言語
- 神谷 英治、
単項二階論理を用いた項書換え系の逐次性判定システム
- 寺澤 啓司、
オブジェクト指向計算モデルにおける例外処理の形式化
- 豊田 隆司、
書換え系を書き換えるMRCプログラムの開発環境
- 伊藤 真洋、
π計算に基づく並行プログラム向けツールキットの作成
- 江場 雅彦、
型のないオブジェクト指向プログラムの代数的意味記述に関する研究
- 大島 淳史、
弁別ネットを用いたメタ項書換え計算インタプリタの設計と実装
- 木川 泰夫、
Hennessy-Milner論理に基づく通信プロセスの文脈依存特性化
- 二井 靖彦、
代数的仕様における振舞等価性証明のための線形文脈帰納法について
- 宮下 大、
自動ラベル付けに基づく項書換え系の合流性の判定
- 平手 孝、
通信プロセスのテスト等価性検証のための視覚的支援環境
- 大野 健治、
項書換え系における停止性のモジュラー性に関する研究
- 西村 徹、
直交な条件付き書換え系の合流性
- 大久保 信康、
形式仕様記述に基づく通信プログラム開発システムに関する研究
- 渡辺 啓嗣、
高階項書換え系の停止性に関する研究
- 安保 和幸、
Javaバイトコードに対するメソッド呼出しの直接束縛化