TOP Page >  Profile

To Lab's Site


Full text / JAIST Repository



Kazuhiro Ogata Professor
School of Information Science、Intelligent Robotics Area


Ph.D.from Keio University (1995)


Computer Science, Software engineering, Formal methods

■Research Keywords

model checking, rewriting, specification, theorem proving, verification

■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.



  • Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016,Kazuhiro Ogata, Mark Lawford, Shaoying Liu,Springer,2016,312
  • Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi,Shusaku Iida, Jos?Meseguer, Kazuhiro Ogata (Eds.),Lecture Notes in Computer Science 8373, Springer 2014, ISBN 978-3-642-54623-5,2014

◇Published Papers

  • 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

Display All

◇Lectures and Presentations

  • An attempt toward conjecturing lemmas with graphical animations of state machines,Kazuhiro Ogata,The Second International Lecture Series of School of Software and Microelectornics (SSM), Northwestern Polytechnic University,Xi'an, China,Sept 19-20, 2017
  • A Case Study on Extracting the Characteristics of the Reachable States of a State Machine formalizing a Communication Protocol with Inductive Logic Programing,Dung Tuan Ho, Min Zhang, Kazuhiro Ogata,25th International Conference on Inductive Logic Programming,京都,2015/8/20-22
  • Specification and verification of a single-track railroad signaling in CafeOBJ,Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi,200 International Technical Conference on Circuts/Systems, Computers and Communications (ITC-CSCC 2000)

Display All

■Extramural Activities

◇Other Activities

  • International Conference on Formal Engineering Methods,Steering Committee Member,2019/01/01 - 2019/12/31
  • Journal of Robotics (Hindawi),Guest Editor Special Issue,2017/10/01 - 2018/12/31
  • 7th International Conference on Software and Computer Applications (ICSCA 2018),PC member,2017/11/01 - 2018/02/28

Display All

■Academic Awards Received

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