TOP  >  Personal Info.
OGATA, Kazuhiro Professor, Director of Research Center for Integrated Science
Information Science, Computing Science, Research Center for Advanced Computing Infrastructure
◆Degrees
Ph.D.from Keio University (1995)
◆Specialties
Software
◆Research Keywords
verification, theorem proving, specification, rewriting, model checking
◆Research Interests
Formal verification with the OTS/CafeOBJ method
The OTS/CafeOBJ method is a modeling, specification and verification method for systems. Observational transition systems, or OTSs are used as mathematical models of systems. OTSs are written in CafeOBJ, an algebraic specification language/system, and it is verified that OTSs satisfy properties by writing proof plans called proof scores in CafeOBJ and checking them with CafeOBJ.

○Large specifications: Unless an algebraic specification language cannot process large specifications efficiently, we cannot use the specification language for practical purpose. A large specification usually consists of a large number of modules. Therefore, the abstract machine has to process a large number of modules, i.e. a module system, efficiently.

○Fast rewriting: A processor for specification languages should perform fast rewriting so that we can verify specifications and execute them as programs efficiently. Therefore, the abstract machine has to provide some good mechanism for fast rewriting so that we can implement fast rewrite engine that could have the same performance as functional languages.

■Publications

◆Published Papers
Formal analysis of RFC 8120 authentication protocol for HTTP under different assumptions
Naomi Okumura, Kazuhiro Ogata, Yoichi Shinoda
JOURNAL OF INFORMATION SECURITY AND APPLICATIONS, 53, 102529-102529, 2020
A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions
Kazuhiro Ogata
FRONTIERS OF COMPUTER SCIENCE, 13, 1, 51-72, 2019
Formal analysis of a security protocol for e-passports based on rewrite theory specifications
Manjukeshwar Reddy Mandadi, Varuneshwar Reddy Mandadi, Kazuhiro Ogata
JOURNAL OF INFORMATION SECURITY AND APPLICATIONS, 42, 71-86, 2018
Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores
Adrian Riesco, Kazuhiro Ogata
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 27, 2, 6-32, 2018
From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories
Min Zhang, Kazuhiro Ogata
THEORETICAL COMPUTER SCIENCE, 722, 52-75, 2018
◆Misc
A divide and conquer approach to leads-to-model checking
Yati Phyo, Canh Minh Do, Ogata Kazuhiro
ITNOW, 63, 2, 66-, 2021
Specification and verification of real-time multitasking systems by the OTS/CafeOBJ method
東 周輝, 中村 正樹, 榊原 一紀, 緒方 和博
電子情報通信学会技術研究報告 = IEICE technical report : 信学技報, 119, 470, 25-30, 2020
Specification description of real-time multitask systems by the OTS/CafeOBJ method
東 周輝, 中村 正樹, 榊原 一紀, 緒方 和博
電子情報通信学会技術研究報告 = IEICE technical report : 信学技報, 118, 499, 13-18, 2019
ソフトウェアサイエンス研究会（SS研）の紹介
緒方 和博
情報・システムソサイエティ誌, 21, 3, 8-9, 2016
Sufficient completeness of constructor-based order-sorted parameterized specifications
NAKAMURA Masaki, MIRCEA GAINA Daniel, OGATA Kazuhiro, FUTATSUGI Kokichi
Technical report of IEICE. SS, 114, 510, 1-6, 2015
◆Books
Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016
編者(編著者) , 312, Springer, 2016
Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi
編者(編著者) , Lecture Notes in Computer Science 8373, Springer 2014, ISBN 978-3-642-54623-5, 2014
電子情報通信学会「知識ベース」
分担執筆, 2010
◆Conference Activities & Talks
An attempt toward conjecturing lemmas with graphical animations of state machines
The Second International Lecture Series of School of Software and Microelectornics (SSM), Northwestern Polytechnic University, Xi'an, China, 2017
A Case Study on Extracting the Characteristics of the Reachable States of a State Machine formalizing a Communication Protocol with Inductive Logic Programing
25th International Conference on Inductive Logic Programming, 京都, 2015
不変性モデル検査器としてのCafeOBJ
2012年電子情報通信学会ソサイエティ大会, 富山市, 2012
有界モデル検査と帰納法の組合せによる NSPK 認証プロトコルの合意性
ソフトウェア・シンポジウム 2012, 福井市, 2012
CafeOBJによるシステム検証
情報処理学会ソフトウェア工学研究会第165回研究会, JAIST, 2009

■Teaching Experience

Information Processing Theory(E), Algebraic Formal Methods(E), Software Design Methodology(E), Functional Programming, 情報処理論(E), 代数フォーマルメソッド(E), ソフトウェア設計論(E), 関数プログラミング

■Contributions to  Society

◆Academic Contribution
Review Editor on the Editorial Board of Computer Security , Frontiers in Computer Science , 2020
PC co-chair , 32nd International Conference on Software Engineering & Knowledge Engineering , 2020 - 2020
PC co-chair , Fifith IEEE International Conference on Dependable Systems and Their Applications , 2018 - 2018 , Dalian, China
◆Committee Memberships
・ 石川県教育委員会 , 「いしかわ高校科学グランプリ」における運営指導委員 , 2014-

■Academic  Awards

・ BEST PAPER AWARD , The Second IEEE International Symposium on Dependable Computing and Internet of Things (DICT 2015) , 2015