Kazuhiro Ogata
Professor
School of Information Scienceã€Intelligent Robotics Area
Japan Advanced Institute of Science And Technology
Japan
Biography
â– Degrees Ph.D.from Keio University (1995) â– Specialties Computer Science, Software engineering, Formal methods â– Research Keywords model checking, rewriting, specification, theorem proving, verification
Research Interest
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.