Curriculum Vitae of
Kazuhiro OGATA
Professor
School of Information Science
Japan Advanced Institute of Science and Technology (JAIST)
1-1 Asahidai, Tastunokuchi, Nomi, 923-1292 JAPAN
Phone +81-761-51-1211
Fax +81-761-51-1149
Email ogata [at] jaist [dot] ac [dot] jp
1. academic qualification
1995 Doctor of Engineering from Graduate School of Science andTechnology, Keio University
Title of thesis: MultithreadSmalltalk: A Study on Parallelizing Smalltalk
Supervisor: Norihisa DOI
2. working history
1995 - 2001 Research Associate at JAIST2001 - 2002 Researcher at SRA Key Technology Laboratory
2002 - 2006 Research Expert at NEC Software Hokuriku, Ltd.
2006 - 2008 Research Associate Professor at JAIST2009 - July 2014 Associate Professor at JAISTAug 2014 Professor at JAIST
3. academic activities- A lecturer of Sinaia School of Formal Verification of Software
Systems, March 3 - March 10, 2008(http://www.imar.ro/~diacon/sinaiaschool.html)- Co-organizer and a lecturer of JAIST Advanced School on Formal
Specification and Systems Verification 2010 (JAIST-FSSV2010), March 1- March 5, 2010 (http://www.ldl.jaist.ac.jp/jaist-fssv2010/)- Associate editor of IEICE Transactions on Information and Systems,
2007-2011- A program committee member of Automated Formal Methods (AFM)
Workshop 2008 (July 14) and 2009 (June 27)- A program committee member of IEEE International Workshop UML andFormal Methods (UML&FM) 2008 (Oct. 27), 2009 (Dec. 8), 2010 (Nov. 16),and 2011 (June 20)- A program committee member of International Workshop on Rewriting
Logic and its Applications (9th WRLA), March 24 - March 25, 2012,(10th WRLA), April 5 - April 6, 2014, (11th WRLA), April 2 - April 3,
2016- Workshop/tutorial co-chair of 14th International Conference on
Formal Engineering Methods (14th ICFEM), Nov. 12 - Nov. 16, 2012
- Guest editor-in-chief of Special Section of Formal Approach, IEICE
Transactions on Information and Systems, E96-D(6), June, 20131

- Co-chair of Specification, Algebra, and Software: A Festschrift
Symposium in Honor of Kokichi Futatsugi (SAS 2014), Apr. 14 (Mon) - 16(Wed), 2014, Kanazawa, Japan(http://www.ldl.jaist.ac.jp/futatsugifest/)- A program committe member of International Workshop on SOFL-MSVL(5th SOFL+MSVL), Nov. 6, 2014, (6th SOFL+MSVL), Nov 6, 2015, (7th
SOFL+MSVL), Nov. 15, 2016
- A program committee member of 25th International Symposium on
Logic-Based Program Synthesis and Transformation (LOPSTR 2015), July
13 - July 15, 2015, Siena, Italy- A program committee member of 2nd International Symposium on
Dependable Computing and Internet of Things (DCIT 2015), Nov. 16 Nov. 19, 2015, Wuhan, China- Vice-chair of special interest group of software science (sigss),
IEICE, May 2014 - May 2016
- Chair of special interest group of software science (sigss),
IEICE, May 2016 - May 2018
- A program co-chair of 18th International Conference on Formal
Engineering Methods (ICFEM 2016), Nov. 14 - Nov. 18, 2016, Tokyo,Japan- A program committee member of International Workshop on Formal
Techniques for Safety-Critical Systems (5th FTSCS), Nov. 14, 2016,
Tokyo, Japan- Reviewers of many international journals/conferences, such as ACM
Transactions on Programming Languages and Systems (TOPLAS),
Theoretical Computer Science (TCS), Science of Computer Programming(CSP), and International Conference on Software Engineering (ICSE).
4. research projects
As a principal investigator:
FY2014 - FY2016 Grant-in-Aid for Challenging Exploratory Research,
30272991, A study on model checking distributed algorithms whose
computational targets are distributed systems
FY2011 - FY2013 Grant-in-Aid for Scientific Research (C), 23500041,
Improvement of liveness model checking made infeasible by longproperty formulas
FY2006 - FY2008 Grant-in-Aid for Scientific Research (C), 18500019,
Methodology and Environment for Effectively Using Theorem Provers andModel Checkers
FY2000 - FY2001 Grant-in-Aid for Encouragement of Scientists (A),
12780206, A Study on Specification, Verification and Implementation of
Reactive Systems
FY1998 - FY1999 Grant-in-Aid for Encouragement of Scientists (A),30272991, A Study on Optimizing Compilers for Term Rewriting2

Systems
As a co-investigator:
FY2014 - FY2019 Grant-in-Aid for Scientific Research (A), 90264960, A
Study on Highly Reliable Agile Formal Engineering Methods for Software
Development, Shaoying Liu (principal investigator)
FY2011 - FY2015 Grant-in-Aid for Scientific Research (S), 23220002,
Development of an Innovative Specification Verification System based on
Proof Scores, Kokichi Futatsugi (principal investigator)
FY2000 - FY2003 Grant-in-Aid for Scientific Research on Priority
Areas, 12133206, Safety Verification Technologies based on Behavioral
Specifications, Kokichi Futatsugi (principal investigator)
FY1999 - FY2001 Grant-in-Aid for Exploratory Research, 11878050, A
Study on Coordination Models based on Module Systems, Kokichi
Futatsugi (principal investigator)
FY1998 - FY2001 Grant-in-Aid for Scientific Research (B), 10558043,
Development of Formal Specification Language for Writing
Specifications as Components Based on Functions, Kokichi Futatsugi(principal investigator)
FY1995 - FY1997 Grant-in-Aid for Scientific Research (B), 07458056, A
Study on Abstract Machines for Concurrent Rewriting, Kokichi Futatsugi(principal investigator)
FY2006 - FY2008 Specific Research Grant A, Discipline 2 (Physics andInformation), The Asahi Glass Foundation, Automating Security Analysesof Electric Commerce Protocols, Kokichi Futatsugi (principal
investigator)
5. publications[journal papers][1] Takahiro Seino, Kazuhiro Ogata and Kokichi Futatsugi:
Specification and verification of a single-track railroad signaling in
CafeOBJ, IEICE TRANSACTIONS on Fundamental of Electronics,
Communications and Computer Science, E84-A(6): 1471-1478, IEICE, 2001.
[2] Kazuhiro Ogata and Kokichi Futatsugi: Flaw and modification of theiKP electronic payment protocols, Information Processing Letters,
86(2): 57-62, Elsevier, 2003.
[3] Razvan Diaconescu, Kokichi Futatsugi and Kazuhiro Ogata: CafeOBJ:
Logical Foundation and Methodologies, Computing and Informatics,
22(3): 257-283, Slovak Academic Press, 2003.
[4] Takahiro Seino, Kazuhiro Ogata and Kokichi Futatsugi: MechanicallySupporting Case Analysis for Verification of Distributed Systems,
Journal of Pervasive Computing and Communications, 1(2): 135-145,
Troubador, 2005.
[5] Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi: Specification
and Verification of Workflows with RBAC Mechanism and SoD Constraints,
International Journal of Software Engineering and Knowledge

3

Engineering, 17(1): 3-32, World Scientific, 2007.
[6] Kazuhiro Ogata and Kokichi Futatsugi: Modeling and verification ofreal-time systems based on equations, Science of Computer Programming,
66(2): 162-180, Elsevier, 2007.
[7] Kazuhiro Ogata and Kokichi Futatsugi: Comparison of Maude and SAL
by Conducting Case Studies Model Checking a Distributed Algorithm,
IEICE TRANSACTIONS on Fundamental of Electronics, Communications andComputer Science, E90-A(8): 1690-1703, IEICE, 2007.
[8] Kazuhiro Ogata and Kokichi Futatsugi: State Machines as Inductive
Types, IEICE TRANSACTIONS on Fundamental of Electronics,
Communications and Computer Science, E90-A(12): 2985-2988, IEICE,
2007.
[9] Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura and Kokichi
Futatsugi: Creme: An Automatic Invariant Prover of Behavioral
Specifications, International Journal of Software Engineering andKnowledge Engineering, 17(6): 783-804, World Scientific, 2007.
[10] Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata and Kokichi
Futatsugi: A Specification Translation from Behavioral Specifications
to Rewrite Specifications, IEICE TRANSACTIONS on Information and
Systems, E91-D(5): 1492-1503, IEICE, 2008.
[11] Kazuhiro Ogata and Kokichi Futatsugi: Proof Score Approach to
Verification of Liveness Properties, IEICE TRANSACTIONS on Informationand Systems, E91-D(12): 2804-2817, IEICE, 2008.
[12] Jianwen Xiang, Jing Tian, Kazuhiro Ogata, Kokichi Futatsugi andAkira Mori: Analysis of membership sharing problem in digital
subscription services, International Journal of Revenue Management,
3(3): 284-306, Inderscience Enterprises Ltd., 2009.
[13] Masaki Nakamura, Kazuhiro Ogata and Kokichi Futatsugi:
User-Defined On-Demand Matching, IEICE TRANSACTIONS on Information and
Systems, E92-D(7): 1401-1411, IEICE, 2009.
[14] Masaki Nakamura, Kazuhiro Ogata and Kokichi Futatsugi:
Reducibility of operation symbols in term rewriting systems and its
application to behavioral specifications, Journal of Symbolic
Computation, 45(5): 551-573, Elsevier, 2010.
[15] Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi: Towards
Reliable E-Government Systems with the OTS/CafeOBJ Method, IEICE
TRANSACTIONS on Information and Systems, E93-D(5): 974-984, IEICE,
2010.
[16] Kazuhiro Ogata and Kokichi Futatsugi: Proof Score Approach to
Analysis of Electronic Commerce Protocols, International Journal of
Software Engineering and Knowledge Engineering, 20(2): 253-287, World
Scientific, 2010.
[17] Min Zhang, Kazuhiro Ogata and Masaki Nakamura: Translation ofState Machines from Equational Theories into Rewrite Theories with
Tool Support, IEICE TRANSACTIONS on Information and Systems, E94-D(5):976-988, IEICE, 2011.

4

[18] Kokichi Futatsugi, Daniel Gaina and Kazuhiro Ogata: Principles of
proof scores in CafeOBJ. Theoretical Computer Science (TCS), 464:90-112, Elsevier, 2012.
[19] Daniel Gaina, Kokichi Futatsugi and Kazuhiro Ogata:
Constructor-based Logics. The Journal of Universal Computer Science(J. UCS), 18(16): 2204-2233, J.UCS consortium, 2012.
[20] Kazuhiro Ogata, Kokichi Futatsugi: Compositionally Writing Proof
Scores of Invariants in the OTS/CafeOBJ Method. The Journal of
Universal Computer Science (J. UCS), 19(6): 771-804, J.UCS consortium,
2013.
[21] Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi: On Proving
Operational Termination Incrementally with Modular Conditional
Dependency Pairs, IAENG International Journal of Computer Science,40(2): 117-123, International Association of Engineers (IAENG), 2013.
[22] Iakovos Ouranos, Petros Stefaneas, Kazuhiro Ogata: TESLA source
authentication protocol verification experiment in the Timed
OTS/CafeOBJ method: Experiences and Lessons Learned, IEICE
TRANSACTIONS on Information and Systems, E97-D(5):1160-1170, IEICE,
2014.
[23] Kazuhiro Ogata, Thapana Chaimanont, Min Zhang: Formal Modelingand Analysis of Time- and Resource-sensitive Simple Business
Processes, Journal of Information Security and Applications (JISA),
31: 23-40, Elsevier, 2016.
[24] Adrian Riesco, Kazuhiro Ogata, Futatsugi Kokishi: A Maude
Environment for CafeOBJ, Formal Aspects of Computing, Springer (FAoC),
2016 (to appear).
[conference papers][1] Kazuhiro Ogata and Norihisa Doi: Knowledge representation andinference - an approach from object-oriented computing and fuzzy
theory -, Proceedings of the 1st Pacific Rim International Conferenceon Artificial Intelligence (1st PRICAI), pp.729-734 (1990).
[2] Kazuhiro Ogata, Satoshi Kurihara, Mikio Inari and Norihisa Doi:
HoME: Smalltalk on Mach environment, Proceedings of the 6thInternational Conference on Technology of Object-Oriented Languages
and Systems (6th TOOLS), Prentice Hall, pp.153-161 (1991).
[3] Kazuhiro Ogata, Satoshi Kurihara, Mikio Inari and Norihisa Doi:
The design and implementation of HoME, Proceedings of the ACM SIGPLAN'92 Conference on Programming Language Design and Implementation (PLDI
1992), SIGPLAN Notices, Vol.27, No.7, ACM Press, pp.44-54 (1992).
[4] Kazuhiro Ogata and Norihisa Doi: Object allocation and dynamic
compilation in MultithreadSmalltalk, Proceedings of the 1994 ACM
Symposium on Applied Computing (SAC 1994), ACM Press, pp.452-456(1994)[5] Kazuhiro Ogata, Koichi Ohhara and Kokichi Futatsugi: TRAM: anabstract machine for order-sorted conditional term rewriting systems,
Proceedings of the 8th International Conference on Rewriting
Techniques and Applications (8th RTA), LNCS 1232, Springer, pp.335-338

5

(1997).
[6] Kazuhiro Ogata and Kokichi Futatsugi: Implementation of term
rewritings with the evaluation strategy, Proceedings of the 9thInternational Symposium on Programming Languages, Implementations,
Logics, and Programs (9th PLILP), LNCS 1292, Springer, pp.225-239(1997).
[7] Kazuhiro Ogata, Masaru Kondo, Shigenori Ioroi and Kokichi
Futatsugi: Design and implementation of Parallel TRAM, Proceedings ofthe 3rd International Euro-Par Conference (3rd Euro-Par), LNCS 1300,
Springer, pp.1209-1216 (1997).
[8] Takashi Nagaya, Michihiro Matsumoto, Kazuhiro Ogata and Kokichi
Futatsugi: How to give local strategies to function symbols forequality of two implementations of the E-strategy with and without
evaluated flags, Proceedings of the 3rd Asian Symposium on Computer
Mathematics (3rd ASCM), Lanzhou University Press, pp.71-81 (1998).
[9] Kazuhiro Ogata, Hiromichi Hirata, Shigenori Ioroi and Kokichi
Futatsugi: Experimental implementation of Parallel TRAM on massively
parallel computer, Proceedings of the 4th International Euro-Par
Conference (4th Euro-Par), LNCS 1470, Springer, pp.846-851 (1998).
[10] Kazuhiro Ogata, Shigenori Ioroi and Kokichi Futatsugi: Optimizing
term rewriting using discrimination nets with specialization,
Proceedings of the 1999 ACM Symposium on Applied Computing (SAC 1999),
ACM Press, pp.511-518 (1999).
[11] Kazuhiro Ogata and Kokichi Futatsugi: Specification andverification of some classical mutual exclusion algorithms with
CafeOBJ, Proceedings of the OBJ/CafeOBJ/Maude Workshop at Formal
Methods 1999, Theta, pp.159-177 (1999).
[12] Kazuhiro Ogata and Kokichi Futatsugi: Formal verification of the
MCS list-based queuing lock, Proceedings of the 5th Asian Computing
Science Conference (5th ASIAN), LNCS 1742, Springer, pp.281-293(1999).
[13] Kazuhiro Ogata and Kokichi Futatsugi: Operational semantics ofrewriting with the on-demand evaluation strategy, Proceedings of the2000 ACM Symposium on Applied Computing (SAC 2000), ACM Press,
pp.756-763 (2000).
[14] Masaki Nakamura and Kazuhiro Ogata: The evaluation strategy forhead normal form with and without on-demand flags, Proceedings of the
3rd International Workshop on Rewriting Logic and its Applications(3rd WRLA), ENTCS 36, Elsevier, pp.212-228 (2000).
[15] Kazuhiro Ogata and Kokichi Futatsugi: Specifying and verifying arailroad crossing with CafeOBJ, Proceedings of the 6th International
Workshop on Formal Methods for Parallel Programming: Theory andApplications (6th FMPPTA) (Part of Proceedings of IPDPS 2001), IEEE
Computer Society Press, p.150, (2001).
[16] Kazuhiro Ogata and Kokichi Futatsugi: Modeling and verificationof distributed real-time systems based on CafeOJB, Proceedings of the
16th International Conference on Automated Software Engineering (16thASE), IEEE Computer Society Press, pp.185-192 (2001).

6

[17] Kazuhiro Ogata and Kokichi Futatsugi: Formally modeling andverifying Ricart&Agrawala distributed mutual exclusion algorithm,
Proceedings of the 2nd Asia-Pacific Conference on Quality Software(2nd APAQS), IEEE Computer Society Press, pp.357-366 (2001).
[18] Kazuhiro Ogata and Kokichi Futatsugi: Formal analysis of
Suzuki&Kasami distributed mutual exclusion algorithm, Proceedings ofthe IFIP TC6/WG6.1 5th International Conference on Formal Methods forOpen Object-Based Distributed Systems (5th FMOODS), Kluwer, pp.181-195(2002).
[19] Kazuhiro Ogata and Kokichi Futatsugi: Rewriting-based
verification of authentication protocols, Proceedings of the 4thInternational Workshop on Rewriting Logic and its Applications (4thWRLA), ENTCS 71, Elsevier, pp.189-203 (2004).
[20] Kazuhiro Ogata and Kokichi Futatsugi: Formal verification of theHorn-Preneel micropayment protocol, Proceedings of the 4thInternational Conference on Verification, Model Checking, and Abstract
Interpretation (4th VMCAI), LNCS 2575, Springer, pp.238-252 (2003).
[21] Kazuhiro Ogata and Kokichi Futatsugi: Formal analysis of the iKP
electronic payment protocols, Proceedings of the 1st International
Symposium on Software Security (1st ISSS), LNCS 2609 (Hot Topics,
Software Security - Theories and Systems), Springer, pp.441-460(2003).
[22] Kazuhiro Ogata and Kokichi Futatsugi: Proof Scores in the
OTS/CafeOBJ Method, Proceedings of the 6th IFIP WG6.1 International
Conference on Formal Methods for Open Object-Based Distributed Systems(6th FMOODS), LNCS 2884, Springer, pp.170-184 (2003).
[23] Kazuhiro Ogata, Daigo Yamagishi, Takahiro Seino and Kokichi
Futatsugi: Modeling and Verification of Hybrid Systems Based on
Equations, Proceedings of the IFIP 18th World Computer Congress TC10
Working Conference on Distributed and Parallel Embedded Systems (DIPES
2004), Kluwer, pp.43-52 (2004).
[24] Kazuhiro Ogata and Kokichi Futatsugi: Equational Approach toFormal Verification of SET, Proceedings of the 4th International
Conference on Quality Software (4th QSIC), IEEE Computer Society
Press, pp.50-59 (2004).
[25] Takahiro Seino, Kazuhiro Ogata and Kokichi Futatsugi: Supporting
Case Analysis with Algebraic Specification Languages, Proceedings ofthe 4th International Conference on Computer and Information
Technology (4th CIT), IEEE Computer Society Press, pp.1073-1080(2004).
[26] Weiqiang Kong, Kazuhiro Ogata, Jianwen Xiang, Kokichi Futatsugi:
Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol,
Proceedings of the 4th International Conference on Computer andInformation Technology (4th CIT), IEEE Computer Society Press,
pp.1100-1107 (2004).
[27] Kazuhiro Ogata and Kokichi Futatsugi: Formal Analysis of the
NetBill Electronic Commerce Protocol, Proceedings of the 2nd
International Symposium on Software Security (2nd ISSS), LNCS 3233,

7

Springer, pp.45-64 (2004).
[28] Takahiro Seino, Kazuhiro Ogata and Kokichi Futatsugi: A Toolkit
for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method,
Proceedings of the 6th International Workshop on Rule-Based
Programming (6th RULE), ENTCS 147(1), Elsevier, pp.57-72 (2006).
[29] Kazuhiro Ogata and Kokichi Futatsugi: Equational Approach toFormal Analysis of TLS, Proceedings of the 25th International
Conference on Distributed Computing Systems (25th ICDCS), IEEE
Computer Society Press, pp.795-804 (2005).
[30] Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi: Formal
Analysis of Workflow Systems with Security Considerations, Proceedingsof the 17th International Conference on Software Engineering andKnowledge Engineering (17th SEKE), Knowledge Systems Institute,
pp.531-536 (2005).
[31] Kazuhiro Ogata and Kokichi Futatsugi: Proof Score Approach to
Verification of Liveness Properties, Proceedings of the 17th
International Conference on Software Engineering and Knowledge
Engineering (17th SEKE), Knowledge Systems Institute, pp.608-613(2005).
[32] Jittisak Senachak, Takahiro Seino, Kazuhiro Ogata and Kokichi
Futatsugi: Provably Correct Translation from CafeOBJ into Java,
Proceedings of the 17th International Conference on Software
Engineering and Knowledge Engineering (17th SEKE), Knowledge Systems
Institute, pp.614-619 (2005).
[33] Jianwen Xiang, Kazuhiro Ogata and Kokichi Futatsugi: Formal Fault
Tree Analysis of State Transition Systems, Prceedings of the 5thInternational Conference on Quality Software (5th QSIC), IEEE Computer
Society Press, pp.124-131 (2005).
[34] Kazuhiro Ogata and Kokichi Futatsugi: Analysis of the
Suzuki-Kasami Algorithm with SAL Model Checkers, Proceedings of the
5th International Conference on Computer and Information Technology(5th CIT), IEEE Computer Society Press, pp.937-943 (2005).
[35] Kazuhiro Ogata, Masahiro Nakano, Masaki Nakamura and Kokichi
Futatsugi: Chocolat/SMV: A Translator from CafeOBJ into SMV,
Proceedings of the 6th International Conference on Parallel andDistributed Computing, Applications and Technologies (6th PDCAT), IEEE
Computer Society Press, pp.416-420 (2005).
[36] Kazuhiro Ogata and Kokichi Futatsugi: Analysis of the
Suzuki-Kasami Algorithm with the Maude Model Checker, Proceedings ofthe 12th Asia-Pacific Software Engineering Conference (12th APSEC),IEEE Computer Society Press, pp.159-166 (2005).
[37] Weiqiang Kong, Kazuhiro Ogata, Takahiro Seino and Kokichi
Futatsugi: A Lightweight Integration of Theorem Proving and Model
Checking for System Verification, Proceedings of the 12th Asia-Pacific
Software Engineering Conference (12th APSEC), IEEE Computer Society
Press, pp.59-66 (2005).
[38] Jianwen Xiang, Weiqiang Kong, Kokichi Futatsugi and Kazuhiro
Ogata: Analysis of Positive Incentives for Protecting Secrets in

8

Digital Rights Management, Proceeding of the 2nd International
Conference on Web Information Systems and Technologies (2nd WEBIST),
INSTICC Press, pp.5-12 (2006).
[39] Kazuhiro Ogata and Kokichi Futatsugi: Some Tips on Writing Proof
Scores in the OTS/CafeOBJ Method, Proceedings of the Festschrift
Symposium in Honor of Joseph A. Goguen (Algebra, Meaning, andComputation: Essays Dedicated to Joseph A. Goguen on the Occasion ofHis 65th Birthday), LNCS 4060, Springer, pp.596-615 (2006).
[40] Kazuhiro Ogata, Weiqiang Kong and Kokichi Futatsugi:
Falsification of OTSs by Searches of Bounded Reachable State Spaces,
Proceedings of the 18th International Conference on Software
Engineering and Knowledge Engineering (18th SEKE), Knowledge Systems
Institute, pp.440-445 (2006).
[41] Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura and Kokichi
Futatsugi: Automating Invariant Verification of Behavioral
Specifications, Proceedings of the 6th International Conference on
Quality Software (6th QSIC), IEEE Computer Society Press, pp.49-56(2006).
[42] Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong and Kokichi
Futatsugi: Induction-Guided Falsification, Prceedings of the 8thInternational Conference on Formal Engineering Methods (8th ICFEM),
LNCS 4260, Springer, pp.114-131 (2006).
[43] Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi: Algebraic
Approaches to Formal Analysis of the Mondex Electronic Purse System,
Proceedings of the 6th International Conference on Integrated Formal
Methods (6th IFM), LNCS 4591, Springer, pp.393-412 (2007).
[44] Kazuhiro Ogata and Kokichi Futatsugi: Simulation-based
verification for invariant properties in the OTS/CafeOBJ method,
Proceedings of the 4th International Refinement Workshop (Refine2007), ENTCS 201, Elsevier, pp.127-154 (2008).
[45] Kokichi Futatsugi, Joseph A. Goguen and Kazuhiro Ogata: Verifying
Design with Proof Scores, Proceedings of the 1st International
Conference on Verified Software: Theories, Tools, Experiments (1st
VSTTE), LNCS 4171, Springer, pp.277-290 (2008).
[46] Weiqiang Kong, Kazuhiro Ogata, Jian Chen, and Kokichi Futatsugi:
Trace Anonymity in the OTS/CafeOBJ Method, Proceedings of the 8thInternational Conference on Computer and Information Technology (8thCIT), IEEE Computer Society Press, pp.754-759 (2008).
[47] Kazuhiro Ogata and Kokichi Futatsugi: Formal Analysis of the
Bakery Protocol with Consideration of Nonatomic Reads and Writes,
Proceedings of the 10th International Conference on Formal Engineering
Methods (10th ICFEM), LNCS 5256, Springer, pp.187-206 (2008).
[48] Daniel Gaina, Kazuhiro Ogata and Kokichi Futatsugi:
Constructor-Based Institutions, Proceedings of the 3rd Conference on
Algebra and Coalgebra in Computer Science (3rd CALCO), LNCS 5728,
Springer, pp.398-412 (2009).
[49] Min Zhang and Kazuhiro Ogata: Modular Implementation of aTranslator from Behavioral Specification to Rewrite Theory

9Specification, Proceedings of the 9th International Conference on
Quality Software (9th QSIC), IEEE Computer Society Press, pp.406-411(2009).
[50] Iakovos Ouranos, Petros S. Stefaneas and Kazuhiro Ogata: Formal
Modeling and Verification of Sensor Network Encryption Protocol in the
OTS/CafeOBJ Method, Proceedings of the 4th International Symposium on
Leveraging Applications of Formal Methods, Verification, andValidation (4th ISoLA), Part I, LNCS 6415, Springer, pp.75-89 (2012).
[51] Min Zhang, Kazuhiro Ogata and Masaki Nakamura: Specification
Translation of State Machines from Equational Theories into Rewrite
Theories, Proceedings of the 12th International Conference on Formal
Engineering Methods (12th ICFEM), LNCS 6447, Springer, pp.678-693(2010).
[52] Kazuhiro Ogata and Kokichi Futatsugi: A Combination of Forward
and Backward Reachability Analysis Methods, Proceedings of the 12th
International Conference on Formal Engineering Methods (12th ICFEM),
LNCS 6447, Springer, pp.501-517 (2010).
[53] Iakovos Ouranos, Petros S. Stefaneas and Kazuhiro Ogata: Formal
Analysis of TESLA Protocol in the Timed OTS/CafeOBJ Method,
Proceedings (Part II) of the 5th International Symposium on Leveraging
Applications of Formal Methods, Verification, and Validation (5thISoLA), Part I, LNCS 7610, Springer, pp. 126-142 (2010).
[54] Kazuhiro Ogata and Phan Thi Thanh Huyen: Specification and Model
Checking of the Chandy and Lamport Distributed Snapshot Algorithm in
Rewriting Logic, Proceedings of the 14th International Conference on
Formal Engineering Methods (14th ICFEM), LNCS 7635, Springer,
pp. 87-102 (2012).
[55] Min Zhang, Kazuhiro Ogata: Invariant-preserved Transformation ofState Machines from Equations into Rewrite Rules. Proceedings of the
19th Asia-Pacific Software Engineering Conference (19th APSEC), IEEE,
pp.511-516 (2012).
[56] Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi: An Algebraic
Approach to Formal Analysis of Dynamic Software Updating
Mechanisms. Proceedings of the 19th Asia-Pacific Software Engineering
Conference (19th APSEC), IEEE, pp.664-673 (2012).
[57] Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi: Formalization andVerification of Behavioral Correctness of Dynamic Software Updates,
Proceedings of the 2nd Workshop on Validation Strategies for Software
Evolution (2nd VSSE), ENTCS 294, Elsevier, pp.12-23 (2013).
[58] Kazuhiro Ogata and Min Zhang: A Divide & Conquer Approach toModel Checking of Liveness Properties, Proceedings of the 37th Annual
International Computer Software & Applications Conference (37thCOMPSAC), IEEE Computer Society Press, pp.648-657 (2013).
[59] Kazuhiro Ogata: Model Checking Liveness Properties under Fairness& Anti-fairness Assumptions, Proceedings of the 20th Asia-Pacific
Software Engineering Conference (20th APSEC), IEEE, pp.565-570 (2013).
[60] Min Zhang, Yunja Choi, and Kazuhiro Ogata: A Formal Semantics of
the OSEK/VDX Standard in K Framework and its Applications, Proceedings

10

of the 10th International Workshop on Rewriting Logic and its
Applications (10th WRLA), LNCS 8663, Springer, pp. 280-296 (2014).
[61] Masaki Nakamura, Kazuhiro Ogata, and Kokichi Futatsugi:
Incremental Proofs of Termination, Confluence and Sufficient
Completeness of OBJ Specifications, Specification, Algebra, andSoftware: Essays Dedicated to Kokichi Futatsugi, LNCS 8373, Springer,
pp.92-109 (2014).
[62] Min Zhang, Kazuhiro Ogata, and Kokichi Futatsugi: Verifying the
Design of Dynamic Software Updating in the OTS/CafeOBJ Method,
Specification, Algebra, and Software: Essays Dedicated to Kokichi
Futatsugi, LNCS 8373, Springer, pp.560-577 (2014).
[63] Daniel Gaina, Dorel Lucanu, Kazuhiro Ogata, and Kokichi
Futatsugi: On Automation of OTS/CafeOBJ Method, Specification,
Algebra, and Software: Essays Dedicated to Kokichi Futatsugi, LNCS
8373, Springer, pp.578-602 (2014).
[64] Kazuhiro Ogata, and Kokichi Futatsugi: Theorem Proving Based on
Proof Scores for Rewrite Theory Specifications of OTSs, Specification,
Algebra, and Software: Essays Dedicated to Kokichi Futatsugi, LNCS
8373, Springer, pp.630-656 (2014).
[65] Yunja Choi, Min Zhang, and Kazuhiro Ogata: Evaluation of Maude asa test generation engine for automotive operating systems, Proceedingsof the 21st Asia-Pacific Software Engineering Conference (21st APSEC),
IEEE, pp.295-302 (2014).
[66] Norbert Preining, Kazuhiro Ogata, and Kokichi Futatsugi: Liveness
Properties in CafeOBJ - A Case Study for Meta-Level Specifications,
Proceedings of the 24th International Symposium on Logic-Based Program
Synthesis and Transformation (24th LOPSTR), LNCS 8981, Springer,
pp.182-198 (2014)[67] Hiroyuki Yoshida, Kokichi Futatsugi, Kazuhiro Ogata:
Formalization and Verification of Declarative Cloud Orchestration,
17th International Conference on Formal Engineering Methods (17th
ICFEM), LNCS 9407, Springer, pp.33-49 (2015)[68] Kazuhiro Ogata, Thapana Chaimanont, Min Zhang: Formal Modelingand Analysis of Time- and Resource-sensitive Simple Business
Processes, 2nd International Symposium on Dependable Computing andInternet of Things (2nd DCIT), IEEE, pp.1-10 (2015)[69] Ha Thi Thu Doan, Wenjie Zhang, Min Zhang, Kazuhiro Ogata: Model
Checking Chandy-Lamport Distributed Snapshot Algorithm Revisited1, 2ndInternational Symposium on Dependable Computing and Internet of Things(2nd DCIT), IEEE, pp.30-39 (2015)[70] Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi: Towards a Formal
Approach to Modeling and Verifying the Design of Dynamic Software
Updates, 22nd Asia-Pacific Software Engineering Conference (22nd
APSEC), IEEE, pp.159-166 (2015)[71] Masaki Nakamura, Daniel Gaina, Kazuhiro Ogata, Kokichi Futatsugi:
Proving Sufficient Completeness of Constructor-Based Algebraic
Specifications, 7th International Conference on Computer Science andits Applications (CSA-15) and the International Conference on

11Ubiquitous Information Technologies and Applications (CUTE 2015), LNEE
373, Springer, pp.15-21 (2015)[72] Adrian Riesco, Kazuhiro Ogata, Kokichi Futatsugi: CafeInMaude: A
CafeOBJ Interpreter in Maude. 19th International Conference on
Fundamental Approaches to Software Engineering (19th FASE), LNCS 9633,
Springer, pp.377-380 (2016)[73] Ha Thi Thu Doan, Francois Bonnet, Kazuhiro Ogata: Model Checking
of a Mobile Robots Perpetual Exploration Algorithm, 7th International
Workshop on SOFL+MSVL (7th SOFL+MSVL), LNCS, Springer, to appear.
[editors][1] Shusaku Iida, Jose Meseguer, Kazuhiro Ogata: Specification,
Algebra, and Software - Essays Dedicated to Kokichi Futatsugi. Lecture
Notes in Computer Science 8373, Springer 2014, ISBN 978-3-642-54623-5[2] Kazuhiro Ogata, Mark Lawford, Shaoying Liu: Formal Methods andSoftware Engineering - 18th International Conference on Formal
Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016,
Proceedings. Lecture Notes in Computer Science 10009, 2016, ISBN
978-3-319-47845-6

12