TOP Page >  Faculty List by School >  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

  • Liveness properties in CafeOBJ ?a case study for meta-level specifications,Norbert Preining, Kazuhiro Ogata, and Kokichi Futatsugi,Logic-Based Program Synthesis and Transformation ?24th International Symposium, LOPSTR 2014Lecture Notes in Computer ScienceSpringer,8981,182, 12,2015/03
  • 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

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

  • SOFL+MSVL 2017,Program Committee Member,2017/01/01 - 2017/12/31
  • 25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015),Program Committee Member,2015/01/01 - 2015/12/31
  • 5th International Workshop on SOFL + MSVL,Program Committee Member,2015/01/01 - 2015/12/31

Display All

■Academic Awards Received

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