卒業論文一覧
酒井研（酒井・西田研）卒業生
- 岡部 優翔、
論理制約付き項書換え系への文脈依存性の導入による全パス到達可能性検証の効率化
- 難波 美優、
制約付き書換えにおける複数の項に関する合流性の同時証明のためのナローインググラフとその十分条件
酒井・西田研卒業生
- 宇佐美 海、
CSPソルバSugarのPythonインターフェースへの目的関数の導入
- 河野 透、
演奏感を残したテンポ一定化によるMIDI変換
- 田辺 竣也、
整数状態遷移機械を定義するUppaal記述から論理制約付き項書換え系への変換
- 中村 勇翔、
整数とブール値のみを処理するPython関数から論理制約付き項書換え系への変換
- 伊藤 健太、
時間順バックトラックを併用するCDCL法に基づく投射モデル計数ソルバの設計と実装
- 佐藤 宏志、
拍対応情報の利用による楽譜と実演奏の音符対応情報の自動生成法
- 三浦 健太郎、
副作用を持つ式を含むC言語プログラムから論理制約付き項書換え系への変換
酒井研卒業生
- 天春 陽介、
リズムの木表現に基づく自動採譜における和音を含むMIDIイベント列の分割判定法
- 小熊 優志、
対称性除去に基づく擬ブール制約付き最適化問題解法の効率化
- 小栗 滉介、
レプタイル問題の解の計数と列挙への重み付き投射モデル計数ソルバの応用
- 平等 望、
カット無し限量子無し循環証明と書換え帰納法証明の相互変換の実装
- 熊谷 妃美香、
プログラム逆化のための文脈自由表現の等価関係に基づく項書換え系決定化手法の自動化
- 後藤 円香、
自動演奏への表情付けのための生成音楽理論に基づくフレーズ情報の生成法
- 林 渉、
高速なMalbolge プログラムを生成するための3進シフト命令のコンパイル法
- 松見 歩佳、
ビットベクトル制約付き項書換え系における単一自己ループの停止性証明法の改良と実装
- 平墳 瑠弥、
MIDI からの自動採譜におけるテンポと拍位置の推定
- 葉 翔太、
阻止節追加型投射モデル計数ソルバにおける阻止節縮小法の改良
- 山内 啓輔、
項書換え系の書換え帰納法における推論がダイヤモンド性を持つための条件
- 赤尾 健太、
自動採譜における木オートマトンに基づくリズム量子化への休符処理の導入
- 加藤 拓洋、
whileプログラムのLLVM中間コードから論理制約付き項書換え系への変換法
- 小嶋 美咲、
排他制御を含むプログラムから論理制約付き項書換え系への変換
- 磯貝 孝明、
命題論理式の全ての投射モデルを表現するBDDの構成法
- 加藤 諒、
SQLに基づく組合せ最適化問題記述言語を用いたタイムテーブリング
- 岸 潤一郎、
SQLに基づく組合せ最適化問題記述言語を用いたテストスケジューリング
- 小林 倫也、
値呼び戦略により全ての解が求められる条件付き項書換え系の十分条件
- SHIN Donghoon、
A Proof Assistant for Constrained Rewriting Induction with Lemma Generation Based on Equality Derivation
- 岩金 カナン、
C言語サブセットからMalbolgeへのコンパイラにおける配列処理の実現
- 田端 浩明、
線形マルチボトムアップ木変換器の関数性の決定可能性
- 鶴田 佑太、
正規条件付き項書換え系に対する同時評価型および逐次評価型紐解き変換の合流性に関する性質
- 西江 一志、
書換え解析ツールを利用したC言語プログラムの漸近的計算量と実行命令数の解析
酒井研・関研卒業生
- 金澤 慶明、
項書換え系への変換による条件付き項書換え系の停止性証明法の有効性の評価
- 坂梨 元軌、
C言語サブセットからMalbolge難読コードへのコンパイラの設計と実装
- 武田 健志、
木文法に基づくグラフ圧縮法および圧縮グラフに対する頂点選択問合せ評価法の提案と実装
- 早川 裕斗、
関数型プログラムの停止性証明器への項到達不能性の十分条件の実装
- 前田 侑也、
ナローイング計算木による条件付き項書換え系の合流性証明
- 久保田 直子、
成分分割を用いた投射モデル計数ソルバの閾値に対するモデル数の大小判定への拡張
- 川本 将也、
XPath式からボトムアップ先読み付き決定性選択トップダウン木オートマトンへの変換
- 内田 和孝、
重み付きグラフの閉路の最大値に関する制約の充足可能性問題への変換法とそのパリティゲームへの応用
- 笹野 智裕、
ナローイングによる制約付き依存対変換の改良と実装
- 下野 拓弥、
投射モデル計数におけるCNFの簡約化処理の効果
- 對馬 渓人、
SAT型制約ソルバを利用した線形制約の整数解導出法について
- 長江 悠太郎、
An extension of proof graphs for disjunctive parameterised Boolean equation systems
- 中山 亮太、
オートマトンのクラス等価性証明のための制約付き項書換え系の構成法と補題等式の生成法の提案
- 西村 卓、
TopTreeによる木圧縮法の実装および直接問合せ処理法の提案
- 水谷 慎之介、
配列を入力引数とする関数における不正メモリ参照検出のための分離論理の拡張
坂部研・酒井研卒業生
- 石原 鷹、
拡張線形ボトムアップ木変換器の関数性の多項式時間判定
- 黒田 貴之、
条件付き項書き換え系の末尾再帰形への変換
- 河邉 翔平、
増減演算を行う簡潔なMalbolge低級アセンブリプログラムの開発
- 鈴木 涼介、
DPLL型モデル計数ソルバの投射モデル計数への拡張
- 高山 隆之介、
関係データベースにおける問合せに関するl-多様性のモデル計数ソルバを用いた判定法
- 長尾 貴浩、
制約によるパターン照合記述が可能な制約付き項書き換え系の書換え完全性の判定法
- 平島 侑人、
未解釈関数記号を含む線形整数制約式からプレスブルガー算術式への充足可能性保存変換の実装
- 内田 佑作、
ドビー織機における最小枠数の織方図のSATソルバを用いた発見法
- 太田 浩一、
例外処理を含む関数型プログラムの停止性証明ツールの開発とその評価
- 川本 佳史、
項書換え系における関数等価性を保存する引数切り落としに関する研究
- 佐藤 太貴、
正規表現の同値性判定アルゴリズムにおける簡約の簡易化に基づく高速化
- 中村 陽介、
ビルディングパズルのSATソルバによる解法と基本対称節の有効性の評価
- 柳澤 真志、
条件付き項書換え系の条件除去変換の健全性に関する研究
- 片岡 巧、
手続き型プログラムから制約付き項書換え系への停止性保存変換に関する研究
- 加藤 起騎、
難解言語Malbolgeのワード長の拡大とそのプログラミング支援ツール
- 加藤 友郁、
条件付き項書換え系における書換え規則の決定化のための条件部の並び替えアルゴリズム
- 栗木 隆太朗、
Erlang言語を用いて実装した完備化手続きにおける並列実行の評価
- 永塚 尚紀、
項書換え系における多項式解釈法のためのSAT/SMT符号化に関する研究
- 林 篤弘、
「.」メタ文字を含む正規表現の同値性判定に関する研究
- 神谷 尚史、
単純型付き項書換え系における補パターン生成アルゴリズムの提案
- 小嶋 祐介、
単純型付き項書換え系における引数切り落とし法の改良
- 近藤 隆、
SATソルバを利用した充足可能性判定を支援するSMLライブラリの開発
- 坂井 利光、
語問題を基底等式集合の語問題に帰着可能な等式集合のクラスに関する研究
- 藤社 隼、
SATソルバを利用したスリザーリンクの解法に関する研究
- 中野 靖大、
制約付き項のインスタンスを受理する制約付き木オートマトンの構成法
- 東野 惇一郎、
非線形不等式形ループ不変式の未定係数の算出手法に関する研究
- 青山 知由、
動的監視によるプログラムの実行時安全化
- 安藤 聡、
難解言語Malbolgeにおける加算の効率よい実現について
- 大井 一展、
部分項基準判定アルゴリズムの提案と実装
- 大場 康司、
木準同型写像に基づく制約付き書換え系の等価性証明におけるSATソルバの利用
- 倉田 佳佑、
静的依存対法の適用可能性判定アルゴリズムの効率化と実装
- 小林 裕幸、
整数上の線形制約に対する充足可能性判定ツールの実装と評価
- 尾関 朗、
依存対が右線形右シャローなTRSの停止性判定アルゴリズムの改良
- 高桑 一也、
項書換え系への変換による類似した関数の効率的な検証
- 谷村 直樹、
単純型付き項上の逆辞書式経路順序
- 服部 達哉、
制約付き項書換え系における非停止性の十分条件
- 日野 善信、
基本対称関数を利用したSATソルバの実装と評価
- 松田 絋幸、
静的依存対法の適用可能性判定アルゴリズムに関する研究
- 山下 圭太、
SATソルバを用いた部分項基準の判定ツールの実装と評価
- 河野 証昭、
静的依存対法適用条件の自動判定に関する研究
- 鈴木 翔、
単純型付き項上の辞書式経路順序の改良
- 関 和俊、
let構造を保存する逆関数生成のための複製関数の埋め込みについて
- 長坂 哲、
SATソルバを用いたお絵かきロジックの問題作成支援ツールの設計と実装
- 野村 太志、
制約付き木オートマトンにおける状態の階層化
- 馬場 達也、
プログラムの述語抽象化におけるループ不変式の利用について
- 石垣 達也、
手続き型プログラムから書換え系への変換におけるプログラムの微差の吸収に関する研究
- 小島 芳治、
線形右シャロー文脈依存項書換え系の到達可能性
- 近藤 公康、
行列への変換に基づく文字列書換え系の停止性証明に関する研究
- 蛭牟田 英治、
最左最内戦略に基づいた文脈依存項書換え処理系の高速化
- 御宿 義勝、
静的依存対法による関数プログラムの停止性判定システムの実装
- 吉原 尚吾、
型構成子の自由な追加を許した単純型項書換え系の静的依存対法による停止性証明
- 内山 敬太、
準構成子項書換え系の停止性及び最内停止性に関する研究
- 加藤 輝敏、
単射関数の逆計算項書換え系の完備性に関する研究
- 小林 弘昌、
高階書換え系における型付けによる非停止性の保存に関する研究
- 坂田 翼、
Spi計算における機密性の自動検証に関する研究
- 田中 裕二、
書き換え手法に基づくＣプログラムの検証ツールの実現とその自動化のための考察
- 磯谷 泰巨、
強計算依存対法による高階書換え系の停止性証明
- 近藤 悟、
プログラム生成系GeneSysの実装と効率化手法の考察
- 笹田 悠司、
TRSコンパイラCdimpleへの高階関数機能の組み込み
- 星野 由美、
関数プログラムの停止性証明のための辞書式経路順序
- 水谷 知博、
紐解かれた項書換え系の文脈依存条件の除去に関する研究
- 水野 清貴、
Web上での対話的利用を前提とする推論システムの構成に関する研究
- 村田 俊樹、
部分関数の逆計算への所属制約付き項書換え系の応用
- 山田 晃久、
高階書換え系の変換による停止性証明法に関する研究
- 植村 太一、
プログラム生成系GeneSysによる融合変換のための戦略
- 蒲田 明憲、
制約付き高階等式の帰納的推論に関する研究
- 櫻井 敬大、
引数減少原理に基づいた単純型項書換え系の停止性証明
- 澤田 大輔、
図形書換え系のプログラミングに関する研究
- 古市 祐樹、
オブジェクト計算の例外型推論の実装とJava例外解析への応用
- 三浦 浩一、
依存グラフを用いたナローイング計算の停止性に関する研究
- 森岡 洋祐、
単純型項書換え系における高速最内戦略に関する研究
坂部研卒業生
- 浅井 尚樹、
完備化手続きの停止条件に関する考察
- 岩田 篤史、
項の全正規形を探索するためのTRSコンパイラ
- 近田 慎一郎、
高階完備化手続きに基づくプログラム検証システムの構築
- 飯澤 恒、
例外処理機能付きのオブジェクト指向計算モデルにおける型推論アルゴリズム
- 奥谷 大介、
項書換え系と木オートマトンに基づく暗号プロトコル検証法の共通鍵方式への応用
- 佐伯 昌樹、
Join算法のスコープルールに対応したJoinJAVAコンパイラ
- 伊藤 陽生、
データマイニングのための柔軟なデータ取得、操作を支援するAPIの設計
- 岡本 晃治、
合流性を持たないTRSの計算戦略に関する研究
- 高岸 健、
移動エージェントプログラムの動作表示のためのアニメーション言語
- 蛸島 洋明、
メタ項書き換え計算における単純メタ項の停止性に関する研究
- 村田 龍彦、
木オートマトンに基づく項書き換え系の到達可能性判定ツール
- 森田 洋介、
Proof-carrying code法のコード記述言語の拡張
- 大田 集、
条件付き項書換え系の実行系とプログラムの型推論への応用
- 岡田 泰典、
オートマトン描画ライブラリの設計と実現
- 岡田 有加、
項間の関係の推移的閉包を認識するオートマトン構成法の実現
- 三小田 憲正、
ポスト対応問題の統計的分析
- 中島 年彦、
逆TRSに基づく逆像の計算系の実現
- 長島 正憲、
オートマトン変換系とその状態対応関係の生成に関する研究
- 山本 友和、
潜在帰納法に基づく振るまい等価性の証明系の実現
- 大原 直美、
定理自動証明システム Isabelle を用いたプログラム検証の自動化
- 桑村 大輔、
依存対を用いたTRSの停止性判定システムの実装
- 佐野 嘉則、
定理自動証明系を用いたセキュリティプロトコルの安全性解析に関する研究
- 高梨 理衣子、
Ambient算法のアニメーションによる実行環境の設計と実装
- 徳田 真也、
TRSコンパイラCdimpleの組込み型のマッチング機能に関する研究
- 前田 裕紀、
メモリリークのないCプログラム作成法の比較・評価とその応用
- 原 達彦、
データ型の導入によるオブジェクト指向言語TinyObjectの拡張とその型推論アルゴリズム
- 橋爪 啓明、
メタ項書換え系の合流性判定システムの実装
- 堀 慎一郎、
依存対に基づく項書換え系の停止性に関する研究
- 堀江 美保子、
例外処理機能を持つオブジェクト指向計算モデルとその型システムに関する研究
- 鍛治 征毅、
項書換え系変換のMRCによる実現に関する研究
- 大塚 和明、
CMLによる同期機能付きMRCインタプリタの実装
- 加納 康資、
振舞仕様記述とその検証法に関する研究
- 松岡 大輔、
代数的仕様における振舞等価性証明のための線形文脈帰納法の拡張
- 西田 直樹、
ごみ集めを意識しない利用が可能なライブラリの設計法
- 中村 敏広、
TRSコンパイラに基づく関数型言語の処理系
- 鈴木 剛
優先順序付き項書換え系における逐次戦略のインデックス決定システム
- 早川 香奈子、
メタ項書き換え計算による項書き換え系の等価性判定の自動化
- 石井 宏諭、
結合律と交換律を法とする書換え系の停止性を保証するための順序の研究
- 山田 直広、
高階項の単一化に関する研究
- 白井 基裕、
MRCによるTRS処理プログラミングのための基本ライブラリ開発
- 冨田 泰弘、
ツリーオートマトンに関する研究
- 亀井 政史、
メタ項書換え計算によるKunuth-Bendix完備化アルゴリズムの実現
- 神谷 英治、
時間プロセス言語の順序付きSOS仕様に対する振舞い解析ツール
- 河井 規浩、
項集合書換え系の実現
- 尾関 嘉一郎、
Join-Calculus言語による\\ モバイル通信プロセスのプログラミング
- 谷口 貴啓、
項書換え系のAC停止性に関する研究
- 寺澤 啓司、
オブジェクト指向プログラムの形式モデルに関する基礎的研究
- 山本 亮、
メタ項書換え計算によるオブジェクト指向言語の抽象機械TOMの実行系の実現