連絡先

• 氏名: 田辺良則 (たなべよしのり)
• 所属: 東京大学 大学院情報理工学系研究科 創造情報学専攻
• mail: y-tanabe (atmark) ci (dot) i (dot) u-tokyo (dot) ac (dot) jp
• 公開鍵: こちら

仕事

• Dai Ikarashi, Yoshinori Tanabe, Koki Nishizawa, Masami Hagiya: Modal μ-calculus on min-plus algebra N-infinity, コンピュータソフトウェア (採録決定)
• Vinh Cuong Tran, Yoshinori Tanabe, Masami Hagiya: Abstract Model Checking of Web Applications Using Java PathFinder, Proceedings of the 26th Conference of Japan Society for Software Science and Technology, 2009.
• Yoshinori Tanabe, Masami Hagiya: Games and Natural Number-valued Semantics of the Modal $\mu$-calculus, Proceedings of the 26th Conference of Japan Society for Software Science and Technology, 2009.
• Yoshinori Tanabe and Masami Hagiya: Fixed-point Computations over Functions on Integers with Operations Min, Max and Plus. 6th Workshop on Fixed Points in Computer Science (FICS 2009), Coimbra, Portugal, 12-13 September 2009, pp. 108--115.
• Alexis Goyet, Masami Hagiya, Yoshinori Tanabe: Decidability and Undecidability Results of Modal μ-calculi with N-infinity Semantics. 情報処理学会プログラミング研究会(PRO)．2009年6月．
• Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, Koichi Takahashi: Pre- and Post-conditions Expressed in Variants of the Modal μ-calculus. IEICE Transactions on Information and Systems, Vol.E92-D, No.5, May 2009, pp.995--1002, 2009.
• Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, Koichi Takahashi: Verification of the Deutsch-Schorr-Waite Marking Algorithm with Modal Logic. Second International Conference, Verified Software: Theories, Tools, Experiments (VSTTE 2008), LNCS 5295, pp.115--129, 2008.
• Yoshinori Tanabe, Koichi Takahashi, Masami Hagiya: A decision procedure for alternation-free modal μ-calculi. Advances in Modal Logic, Volume 7 pp. 341--362, 2008.
• Vinh Cuong Tran, Hideki Hashimoto, Yoshinori Tanabe and Masami Hagiya: Verification of Java programs under fairness assumption, Proceedings of the 25th Conference of Japan Society for Software Science and Technology, 2008.
• 田辺良則，高橋孝一: 様相論理を用いた検証手法の並行ごみ集めへの応用． 第6回ディペンダブルシステムワークショップ (DSW'08summer) 論文集, pp.49--53, 2008.
• Dai Ikarashi, Yoshinori Tanabe, Koki Nishizawa, Masami Hagiya: Modal μ-calculus on min-plus algebra N∞. 第10回プログラミングおよびプログラミング言語ワークショップ (PPL2008) 論文集, pp.216--230, 2008. (論文奨励賞受賞)
• Cyrille Artho, Kenji Taguchi, Yasuyuki Tahara, Shinichi Honiden, Yoshinori Tanabe: Specialized Education in Software Model Checking. Formal Methods in Computer Science Education (FORMED2008), pp. 171--179.
• Toshifusa Sekizawa, Yoshinori Tanabe, Yoshifumi Yuasa, Koichi Takahashi: MLAT: A Tool for Heap Analysis Based on Predicate Abstraction by Modal Logic. IASTED International Conference on Software Engineering (SE 2008), pp.310-317, February 2008.
• 五十嵐大, 田辺良則, 西澤弘毅, 萩谷昌己: min-plus代数N∞上の様相μ計算とその応用, 日本ソフトウェア科学会第24回大会, 2007年9月12日
• 湯浅 能史，田辺 良則，関澤 俊弦，高橋 孝一: Agda-MLAT連携による Schorr-Waiteマーキングアルゴリズムの検証 (ポスター) , 日本ソフトウェア科学会第24回大会, 2007年9月13日
• 高橋孝一、田辺良則、関澤俊弦、湯浅能史: 抽象化ツールMLATについて．第3回 システム検証の科学技術シンポジウム. 2006年10月31日
• 木下佳樹, 高橋孝一, 田辺良則, 湯浅能史: 形式的体系の定理証明支援系上での実現法． 第3回システム検証の科学技術シンポジウム, 2006年10月31日. (資料)
• 田辺良則, 萩谷昌己: 階層的グラフ構造の記述と検証のための様相論理. 日本ソフトウェア科学会第23回大会．2006年9月15日
• 湯浅能史, 武山誠, 関澤俊弦, 田辺良則, 高橋孝一: 自動証明系と定理証明支援系の連携によるポインタ操作プログラムの検証について．日本ソフトウェア科学会第23回大会．2006年9月14日
• 田辺良則: 述語抽象化によるアルゴリズムの検証 〜 シェープ解析を例として. 第4回プログラミングおよびプログラミング言語サマースクール, 2006年9月12日． (資料)
• Yoshinori Tanabe: Abstraction of programs manipulating pointers using modal logics (slides) . The Second DIKU-IST Joint Workshop on Foundations of Software. Apr 21, 2006.
• 高橋孝一, 田辺良則, 関澤俊弦: 一次元セルオートマトンの有限近似解析 , コンピュータソフトウェア, Vol.23(2006), No.3 pp.147-157
• 関澤俊弦, 高井利憲, 田辺良則, 高橋孝一: 時相論理の充足可能性判定器のための論理式生成法. 電子情報通信学会論文誌 D, Volume J89-D No.4, pp.642-650, 2006.
• 田辺良則，萩谷昌己: 時間付きグラフ書換系の抽象化について (ポスター). 第８回プログラミングおよびプログラミング言語ワークショップ. 2006年3月6日
• Carl Frederiksen, 田辺良則, 萩谷昌己: 抽象化によるグラフ書換系活性性質検証の一手法 (ポスター). 第８回プログラミングおよびプログラミング言語ワークショップ. 2006年3月6日
• 田辺 良則, 関澤 俊弦, 湯浅 能史, 高橋 孝一: 様相論理を使用したヒープ検証方式 . 第3回ディペンダブルソフトウェアワークショップ (DSW'06), pp.39-50, 2006年1月27日
• 田辺 良則, 関澤 俊弦, 湯浅 能史, 高橋 孝一: 抽象化検証ツールTLATの構築に向けて(ポスター). 第2回「システム検証の科学技術」シンポジウム． 2005年10月21日
• Mitsuharu Yamamoto, Yoshinori Tanabe, Koichi Takahashi, and Masami Hagiya: Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification, IFIP TC2, Verified Software: Theories, Tools, Experiments, 2005.
• Yoshinori Tanabe, Koichi Takahashi, Mitsuharu Yamamoto, Akihiko Tozawa, and Masami Hagiya: A Decision Procedure for the Alternation-free Two-way Modal μ-calculus . TABLEAUX 2005, Lecture Notes in Artificial Intelligence, Vol.3702, 2005, pp.277-291
• 湯浅能史, 田辺良則, 関澤俊弦, 高橋孝一: 時相論理による述語抽象化のための充足可能性判定手続き. 日本ソフトウェア科学会第21回大会 ． 2005年9月13日．
• 高橋孝一, 田辺良則, 関澤俊弦: 一次元セルオートマトンの有限近似解析. 日本ソフトウェア科学会第21回大会 ． 2005年9月13日．
• 田辺良則，高橋孝一，山本光晴，佐藤貴洋，萩谷昌己: BDDを用いた2方向CTL論理式充足可能性決定手続きの実装 ． コンピュータソフトウェア, Vol.22, No.3 (2005), pp.154-166
• Yoshinori Tanabe, Toshinori Takai, Toshifusa Sekizawa, Koichi Takahashi: Preconditions of properties described in CTL for statements manipulating pointers . Supplemental Volume of the 2005 International Conference on Dependable Systems and Networks (DSN-2005), June 28-July 1, 2005, pp.228-234.
• 田辺良則，高橋孝一，山本光晴，佐藤貴洋，戸沢晶彦，萩谷昌己: BDDによる実装が可能な様相論理の充足可能性判定手続き． 第7回プログラミングおよびプログラミング言語ワークショップ (PPL2005) 論文集, 2005, pp.5-16.
• 田辺良則，高井利憲，高橋孝一: 抽象化を用いた検証ツール． コンピュータソフトウェア，Vol.22, No.1 (2005), pp.2-44. (日本ソフトウェア科学会2007年度解説論文賞受賞)
• 高橋孝一，田辺良則，高井利憲，関澤俊弦: ポインタ処理システムのための自動抽象化法 (ポスター)． JST CREST「情報社会を支える新しい高性能情報処理技術」第1回 公開シンポジウム, 2004年12月14日．
• Yoshinori Tanabe: Satisfiability Checking of Temporal Logics for Verification of Pointer Systems (スライド)． CVS/AIST 研究集会シリーズ「検証と書換」 , 2004年10月21日.
• 佐藤 貴洋，田辺 良則，萩谷 昌己: BDDを用いたガード付きフラグメントの充足可能性判定 ． 日本ソフトウェア科学会第21回大会 ． 2004年9月16日．
• 田辺良則, 高橋孝一, 高井利憲: 時相論理式を用いた抽象化法のツール化に向けて (予稿, スライド )． シンポジウム「システム検証の科学技術」． 2004年2月4日〜6日．
• 田辺良則, 高井利憲, 高橋孝一: 抽象化を用いた検証ツールの調査． 産業技術総合研究所算譜科学グループ研究速報 AIST-PS-2003-007. 2003年12月

博士論文

• Yoshinori Tanabe: Satisfiability judgment of modal logics and their application to verification problems (様相論理の充足可能性判定手続きと検証問題への応用). Ph.D thesis, University of Tokyo, March 2008. (pdf)