連絡先
仕事
-
吉岡信和，田辺良則，田原康之，長谷川哲夫，磯部祥尚:
モデル検査による設計検証．
コンピュータ・ソフトウェア．(採録決定)
-
逸見港，田辺良則，今井宜洋，萩谷昌己:
検証済みのコードによるCoqからScalaへのコード抽出．
第31回ソフトウェア科学会大会．(2014年9月10日)
-
坂本一憲, 田辺良則:
ハッカソン形式の実践的IT教育の実施報告．
第31回ソフトウェア科学会大会．(2014年9月8日)
-
島田工，前澤悠太，鄭顕志，田辺良則，本位田真一:
Scalaの並行プログラム検査における状態空間探索手法．
第9回ソフトウェアエンジニアリングシンポジウム (SES2014), 2014.
(ショートペーパー)
-
姜 帆, 田辺 良則, 本位田 真一:
Coq を使用したMapReduce アプリケーションの検証とScala コード．
電子情報通信学会論文誌, Vol.J97-D, No.3, pp.625-634, 2014.
-
逸見港，田辺良則，萩谷昌己:
CoqからScalaへのロバストなコード抽出．
第16回プログラミングおよびプログラミング言語ワークショップ（PPL2014）．
(ポスター．2014年3月6日)
-
逸見港，田辺良則，萩谷昌己:
CoqからScalaへのロバストなコード抽出に向けて．
第11回ディペンダブルソフトウェアワークショップ(DSW2013)．
(ポスター．2013年12月26日)
-
Yuuki Shinobu, Yoshinori Tanabe, and Kazunori Ueda:
Formalization of the Graph Rewriting Operations of LMNtal by Coq.
APLAS 2013 (poster, Dec 10, 2013).
-
古賀陽一郎，田辺良則:
アスペクト指向言語を利用したソフトウェアモデル検査手法．
第20回 ソフトウェア工学の基礎ワークショップ (FOSE 2013)．pp.203-208.
(2013年11月29日)
-
高鶴哲也，今井宜洋，田辺良則:
システム群のBASE特性を保証するためのCoqを用いた検証．
第20回 ソフトウェア工学の基礎ワークショップ (FOSE 2013)．pp.299-300.
(2013年11月29日)
-
前岡 淳, 田辺 良則, 石川 冬樹:
フィールドアクセスに着目したモデル検査の効率化．
第20回 ソフトウェア工学の基礎ワークショップ (FOSE 2013)．pp.311-312.
(2013年11月29日)
-
穂浪勇利，田辺良則，萩谷昌己:
Java PathFinderを使用したOpenFlowコントローラのモデル検査
第30回 ソフトウェア科学会大会．(ポスター．2013年9月12日)
-
信夫裕貴，田辺良則，上田和紀:
LMNtalにおけるグラフ書換え操作のCoqによる形式化
第30回 ソフトウェア科学会大会．(2013年9月13日)
-
前岡 淳, 田辺 良則, 石川 冬樹:
Java PathFinderにおける探索打ち切りポリシーを用いたヒューリスティック探索.
コンピュータ・ソフトウェア 30(3), pp.109-122, 2013.
(pdf)
-
逸見 港, 田辺 良則, 萩谷 昌己:
CoqによるOpenFlowネットワークの形式化とFlowVisorの検証．
第15回プログラミングおよびプログラミング言語ワークショップ（PPL2013）．
(ポスター．2013年3月5日)
-
前岡淳，田辺良則: 実装コード不具合検出へのJava PathFinder適用に向けた探索範囲削減手法の検討．
第19回 ソフトウェア工学の基礎ワークショップ (FOSE 2012)．pp.189-194.
(2012年12月15日)
-
古賀 陽一郎，田辺 良則:
AOPを応用した実用的なソースコードモデル検査手法．
第178回情報処理学会ソフトウェア工学研究発表会．
(2012年11月1日)
-
姜 帆, 田辺 良則, 本位田 真一:
Coqを使用したMapReduceアプリケーションの検証とScalaコードの抽出．
第14回プログラミングおよびプログラミング言語ワークショップ（PPL2012）．
(ポスター．2012年3月9日)
-
田辺 良則, Cyriile Artho, Watcharin Leungwattanakit, 山本 光晴, 萩谷 昌己:
ネットワークアプリケーションのマスター・スレーブ方式モデル検査アルゴリズムについて．
第28回ソフトウェア科学会大会 (2011年9月29日) (高橋奨励賞受賞)
-
小野 洸亮, 田辺 良則, 谷 幹也, 中野 雄介, 野田 夏子, 萩谷 昌己, 平井 洋一, 細野 繁, 蒔原 省吾:
Coq を用いた Hadoop MapReduce アプリケーションの仕様記述とプログラム抽出．
第13回プログラミングおよびプログラミング言語ワークショップ（PPL2011）．
(ポスター．2011年3月10日)
-
Dai Ikarashi, Yoshinori Tanabe, Koki Nishizawa, Masami Hagiya:
Modal μ-calculus on min-plus algebra N-infinity,
コンピュータソフトウェア 27(3), pp.99-113, 2010.
(pdf)
-
田辺良則, Cyrille Artho, 萩谷 昌己, Watcharin Leungwattanakit, 山本 光晴: ネットワークアプリケーションのマスタースレーブ方式によるソフトウェアモデル検査. 第8回ディペンダブルシステムワークショップ (DSW2010summer), 2010.07.20
-
Alexis Goyet, Masami Hagiya and Yoshinori Tanabe: Decidability and undecidability results on the modal mu-calculus with a natural number-valued semantics, Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Lecture Notes in Artificial Intelligence, Vol.6188, 2010, pp.148-160.
-
Yoshinori Tanabe, Vinh Cuong Tran, Masami Hagiya:
Toward Liveness Verification in Java Pathfinder,
第6回ディペンダブルシステムシンポジウム (dss2009), 2009.12.14.
-
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)