| 2025 | PPDP | Folding Narrowing for the Analysis of Mutual Exclusion Protocols. | Ral Lpez-Rueda, Duong Dinh Tran, Canh Minh Do, Santiago Escobar, Kazuhiro Ogata |
| 2025 | SEKE | Formal Specification and Model Checking of the BB84 Protocol in Maude (S). | Canh Minh Do, Kazuhiro Ogata |
| 2025 | SEKE | Formal Specification and Analysis of Post-quantum OpenPGP Protocol in CafeOBJ. | Trong Binh Hoang, Duong Dinh Tran, Canh Minh Do, Kazuhiro Ogata |
| 2024 | ICFEM | A Tableau-Based Approach to Model Checking Linear Temporal Properties. | Canh Minh Do, Tsubasa Takagi, Kazuhiro Ogata |
| 2023 | SEKE | Symbolic Model Checking Quantum Circuits in Maude. | Canh Minh Do, Kazuhiro Ogata |
| 2022 | COMPSAC | IPSG: Invariant Proof Score Generator. | Duong Dinh Tran, Kazuhiro Ogata |
| 2022 | ICFEM | Modeling and verification of the post-quantum key encapsulation mechanism KYBER using Maude. | Vctor Garca, Santiago Escobar, Kazuhiro Ogata |
| 2022 | ICFEM | Formal specification and model checking of lattice-based key encapsulation mechanisms in Maude. | Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani |
| 2022 | ICFEM | Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security analysis. | Duong Dinh Tran, Canh Minh Do, Santiago Escobar, Kazuhiro Ogata |
| 2022 | SEKE | A divide and conquer approach to until and until stable model checking. | Canh Minh Do, Yati Phyo, Kazuhiro Ogata |
| 2022 | SEKE | Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude. | Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani |
| 2021 | COMPSAC | A support tool for the L + 1-layer divide & conquer approach to leads-to model checking. | Yati Phyo, Canh Minh Do, Kazuhiro Ogata |
| 2021 | ICTAC | A Divide & Conquer Approach to Conditional Stable Model Checking. | Yati Phyo, Canh Minh Do, Kazuhiro Ogata |
| 2021 | QRS | Formal Specification and Model Checking of an Autonomous Vehicle Merging Protocol. | Minxuan Liu, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata |
| 2021 | SEKE | Formal verification of Anderson mutual exclusion protocol by introducing an auxiliary variable (S). | Naoki Asae, Duong Dinh Tran, Kazuhiro Ogata |
| 2021 | SEKE | Formal verification of IFF and NSLPK authentication protocols with CiMPG (S). | Thet Wai Mon, Shuho Fujii, Duong Dinh Tran, Kazuhiro Ogata |
| 2021 | SEKE | Formal verification of multitask hybrid systems by the OTS/CafeOBJ method. | Masaki Nakamura, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata |
| 2021 | SEKE | Formal specification and model checking of a recoverable wait-free version of MCS. | Duong Dinh Tran, Kentaro Waki, Kazuhiro Ogata |
| 2020 | APSEC | A divide & conquer approach to testing concurrent programs with JPF | Canh Minh Do, Kazuhiro Ogata |
| 2020 | APSEC | Lemma Weakening for State Machine Invariant Proofs. | Duong Dinh Tran, Dang Duy Bui, Parth Gupta, Kazuhiro Ogata |
| 2020 | ICTAC | CiMPG+F: A Proof Generator and Fixer-Upper for CafeOBJ Specifications. | Adrin Riesco, Kazuhiro Ogata |
| 2020 | QRS | Parallel stratified random testing for concurrent programs. | Canh Minh Do, Kazuhiro Ogata |
| 2020 | SEKE | Formal verification of an abstract version of Anderson protocol with CafeOBJ, CiMPA and CiMPG. | Duong Dinh Tran, Kazuhiro Ogata |
| 2019 | FASE | KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs. | Jiaqi Qian, Min Zhang, Yi Wang, Kazuhiro Ogata |
| 2019 | SEKE | Formal Specification and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S). | Moe Nandi Aung, Yati Phyo, Kazuhiro Ogata |
| 2019 | SEKE | Specification-based Testing with Simulation Relations (S). | Canh Minh Do, Kazuhiro Ogata |
| 2019 | SEKE | Formal Specification and Model Checking of A* Algorithm. | Kazuhiro Ogata |
| 2019 | SSS | An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms. | Ha Thi Thu Doan, Adrin Riesco, Kazuhiro Ogata |
| 2018 | APSEC | Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks. | Yati Phyo, Kazuhiro Ogata |
| 2017 | APSEC | Writing Concurrent Java Programs Based on CafeOBJ Specifications. | Xuan-Linh Ha, Kazuhiro Ogata |
| 2017 | DASC | Graphical Animations of State Machines. | Tam Thi Thanh Nguyen, Kazuhiro Ogata |
| 2017 | ICDCS | Specifying a Distributed Snapshot Algorithm as a Meta-Program and Model Checking it at Meta-Level. | Ha Thi Thu Doan, Kazuhiro Ogata, Franois Bonnet |
| 2017 | ICTAC | A Formal Proof Generator from Semi-formal Proof Documents. | Adrin Riesco, Kazuhiro Ogata |
| 2017 | OPODIS | Model Checking of Robot Gathering. | Ha Thi Thu Doan, Franois Bonnet, Kazuhiro Ogata |
| 2016 | FASE | CafeInMaude: A CafeOBJ Interpreter in Maude. | Adrin Riesco, Kazuhiro Ogata, Kokichi Futatsugi |
| 2015 | APSEC | Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates. | Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi |
| 2015 | ICFEM | Formalization and Verification of Declarative Cloud Orchestration. | Hiroyuki Yoshida, Kazuhiro Ogata, Kokichi Futatsugi |
| 2015 | ILP | Case Studies on Extracting the Characteristics of the Reachable States of State Machines Formalizing Communication Protocols with Inductive Logic Programing. | Dung Tuan Ho, Min Zhang, Kazuhiro Ogata |
| 2014 | APSEC | Evaluation of Maude as a Test Generation Engine for Automotive Operating Systems. | Yunja Choi, Min Zhang, Kazuhiro Ogata |
| 2014 | LOPSTR | Liveness Properties in CafeOBJ - A Case Study for Meta-Level Specifications. | Norbert Preining, Kazuhiro Ogata, Kokichi Futatsugi |
| 2013 | APSEC | Model Checking Liveness Properties under Fairness & Anti-fairness Assumptions. | Kazuhiro Ogata |
| 2013 | COMPSAC | A Divide and Conquer Approach to Model Checking of Liveness Properties. | Kazuhiro Ogata, Min Zhang |
| 2012 | APSEC | Invariant-preserved Transformation of State Machines from Equations into Rewrite Rules. | Min Zhang, Kazuhiro Ogata |
| 2012 | APSEC | An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms. | Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi |
| 2012 | ICFEM | Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic. | Kazuhiro Ogata, Thi Thanh Huyen Phan |
| 2012 | ISoLA | Formal Analysis of TESLA Protocol in the Timed OTS/CafeOBJ Method. | Iakovos Ouranos, Kazuhiro Ogata, Petros S. Stefaneas |
| 2010 | ICFEM | A Combination of Forward and Backward Reachability Analysis Methods. | Kazuhiro Ogata, Kokichi Futatsugi |
| 2010 | ICFEM | Specification Translation of State Machines from Equational Theories into Rewrite Theories. | Min Zhang, Kazuhiro Ogata, Masaki Nakamura |
| 2010 | ISoLA | Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method. | Iakovos Ouranos, Petros S. Stefaneas, Kazuhiro Ogata |
| 2009 | CALCO | Constructor-Based Institutions. | Daniel Gin, Kokichi Futatsugi, Kazuhiro Ogata |
| 2008 | ICFEM | Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes. | Kazuhiro Ogata, Kokichi Futatsugi |
| 2007 | ISCAS | Adaptive Search Range Motion Estimation Algorithm for H.264/AVC. | Tian Song, Kazuhiro Ogata, Kosuke Saito, Takashi Shimamoto |
| 2007 | IFM | Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System. | Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi |
| 2006 | ICFEM | Induction-Guided Falsification. | Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi |
| 2006 | SEKE | Falsification of OTSs by Searches of Bounded Reachable State Spaces. | Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi |
| 2006 | WEBIST | Analysis of Positive Incentives for Protecting Secrets in Digital Rights Management. | Jianwen Xiang, Weiqiang Kong, Kokichi Futatsugi, Kazuhiro Ogata |
| 2005 | APSEC | A Lightweight Integration of Theorem Proving and Model Checking for System Verification. | Weiqiang Kong, Takahiro Seino, Kokichi Futatsugi, Kazuhiro Ogata |
| 2005 | APSEC | Analysis of the Suzuki-Kasami Algorithm with the Maude Model Checker. | Kazuhiro Ogata, Kokichi Futatsugi |
| 2005 | ICDCS | Equational Approach to Formal Analysis of TLS. | Kazuhiro Ogata, Kokichi Futatsugi |
| 2005 | PDCAT | Chocolat/SMV: A Translator from CafeOBJ into SMV. | Kazuhiro Ogata, Masahiro Nakano, Masaki Nakamura, Kokichi Futatsugi |
| 2005 | SEKE | Formal Analysis of Workflow Systems with Security Considerations. | Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi |
| 2005 | SEKE | Proof Score Approach to Verification of Liveness Properties. | Kazuhiro Ogata, Kokichi Futatsugi |
| 2005 | SEKE | Provably Correct Translation from CafeOBJ into Java. | Jittisak Senachak, Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi |
| 2003 | VMCAI | Formal Verification of the Horn-Preneel Micropayment Protocol. | Kazuhiro Ogata, Kokichi Futatsugi |
| 2000 | SAC | Operational Semantics of Rewriting with the On-demand Evaluation Strategy. | Kazuhiro Ogata, Kokichi Futatsugi |
| 1999 | SAC | Optimizing Term Rewriting Using Discrimination Nets With Specialization. | Kazuhiro Ogata, Shigenori Ioroi, Kokichi Futatsugi |
| 1998 | EuroPar | Experimental Implementation of Parallel TRAM on Massively Parallel Computer. | Kazuhiro Ogata, Hiromichi Hirata, Shigenori Ioroi, Kokichi Futatsugi |
| 1997 | EuroPar | Design and Implementation of Parallel TRAM. | Kazuhiro Ogata, Masaru Kondo, Shigenori Ioroi, Kokichi Futatsugi |
| 1994 | SAC | Object allocation and dynamic compilation in MultithreadSmalltalk. | Kazuhiro Ogata, Norihisa Doi |
| 1992 | PLDI | The Design and Implementation of HoME. | Kazuhiro Ogata, Satoshi Kurihara, Mikio Inari, Norihisa Doi |