緒方　和博（オガタ　カズヒロ）　准教授
情報科学研究科（情報科学専攻・理論情報科学領域）

■学位

慶應義塾大学工学士 (1990)，慶應義塾大学工学修士 (1992)，慶應義塾大学博士(工学) (1995)

■専門分野

ソフトウェア工学，形式手法，検証

■研究テーマのキーワード

model checking, rewriting, specification, theorem proving, verification

■研究課題

OTS/CafeOBJ法による形式検証
OTS/CafeOBJ法は，システムのモデル化，仕様記述および検証のための方法である．観測遷移機械としてシステムの数学モデルを作成する．観測遷移機械は，代数仕様言語CafeOBJで記述される．観測遷移機械が所望の性質を満足することを示す証明(証明譜と呼ぶ)をCafeOBJで記述し，証明の正しさをCafeOBJを用いて確認する．

■研究業績

◇発表論文

Automating Invariant Verification of Behavioral Specifications，Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, and Kokichi Futatsugi ，In Proceedings of The Sixth IEEE International Conference on Quality Software (QSIC2006)，pp. 49-56，Oct. 2006
A complete specification transformation from OTS/CafeOBJ to OTS/Maude，Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi，信学技報 IEICE Technical Report，SS2006，13，pp. 1-6，JUNE 2006
Chocolat/SMV: A Translator from CafeOBJ into SMV，Kazuhiro Ogata, Masahiro Nakano, Masaki Nakamura, Kokichi Futatsugi， Proceedings of the 6th International Conference on Parallel and Distributed Computing Applications and Technologies (6th PDCAT), IEEE Computer Society Press，pp.416-420，Dec 2005

全件表示

◇講演発表

不変性モデル検査器としてのCafeOBJ，緒方和博，2012年電子情報通信学会ソサイエティ大会，富山市，2012年9月11日（火）～14日（金）
有界モデル検査と帰納法の組合せによる NSPK 認証プロトコルの合意性，緒方和博，ソフトウェア・シンポジウム 2012，福井市，2012 年 6 月 12 日 (火曜日) ～ 14 日 (木曜日)
代数仕様言語・処理系のシステム検証への応用，緒方和博，ソフトウェアシンポジウム２００９、ソフトウェア技術者協会，札幌，2009年6月17日～6月19日

全件表示

■担当講義

ソフトウェア設計論(E)，関数プログラミング

■学外活動

◇その他の国際・国内貢献等

International Conference on Formal Engineering Methods，Co-workshop Chair
電子情報通信学会，フォーマルアプローチ特集編集委員長，2012/03/01 - 2013/02/28

緒方 和博 （オガタ カズヒロ） 准教授 情報科学研究科（情報科学専攻・理論情報科学領域）

■学位