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)


Software engineering, Formal methods, Verification

■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

  • 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)
  • The evaluation strategy for head normal form with and without on-demand flags,Masaki Nakamura, Kazuhiro Ogata,The 3rd International Workshop on Rewriting Logic and its Applications (WRLA 2000)

Display All

■Extramural Activities

◇Other Activities

  • IEEE 2nd International Symposium on Dependable Computing and Internet of Things,Program Committee Member,2015/01/01 - 2015/12/31
  • 5th International Workshop on SOFL + MSVL,Program Committee Member,2015/01/01 - 2015/12/31
  • 25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015),Program Committee Member,2015/01/01 - 2015/12/31

Display All