The Design and Implementation of HoME. - Kazuhiro Ogata 001; Satoshi Kurihara; Mikio Inari; Norihisa Doi (PLDI, 1992)

HoME: Smalltalk on the Match Environment. - Kazuhiro Ogata 001; Satoshi Kurihara; Mikio Inari; Norihisa Doi (TOOLS (6), 1992)

Object allocation and dynamic compilation in MultithreadSmalltalk. - Kazuhiro Ogata 001; Norihisa Doi (SAC, 1994)

Design and Implementation of Parallel TRAM. - Kazuhiro Ogata 001; Masaru Kondo; Shigenori Ioroi; Kokichi Futatsugi (Euro-Par, 1997)

Implementation of Term Rewritings with the Evaluation Strategy. - Kazuhiro Ogata 001; Kokichi Futatsugi (PLILP, 1997)

TRAM: An Abstract Machine for Order-Sorted Conditioned Term Rewriting Systems. - Kazuhiro Ogata 001; Koichi Ohhara; Kokichi Futatsugi (RTA, 1997)

Experimental Implementation of Parallel TRAM on Massively Parallel Computer. - Kazuhiro Ogata 001; Hiromichi Hirata; Shigenori Ioroi; Kokichi Futatsugi (Euro-Par, 1998)

Formal Verification of the MCS List-Based Queuing Lock. - Kazuhiro Ogata 001; Kokichi Futatsugi (ASIAN, 1999)

Optimizing Term Rewriting Using Discrimination Nets With Specialization. - Kazuhiro Ogata 001; Shigenori Ioroi; Kokichi Futatsugi (SAC, 1999)

Operational Semantics of Rewriting with the On-demand Evaluation Strategy. - Kazuhiro Ogata 001; Kokichi Futatsugi (SAC (2), 2000)

The evaluation strategy for head normal form with and without on-demand flags. - Masaki Nakamura 001; Kazuhiro Ogata 001 (WRLA, 2000)

Formally Modeling and Verifying Ricart&Agrawala Distributed Mutual Exclusion Algorithm. - Kazuhiro Ogata 001; Kokichi Futatsugi (APAQS, 2001)

Specifying and verifying a railroad crossing with CafeOBJ. - Kazuhiro Ogata 001; Kokichi Futatsugi (IPDPS, 2001)

Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ. - Kazuhiro Ogata 001; Kokichi Futatsugi (ASE, 2001)

Formal Analysis of Suzuki & Kasami Distributed Mutual Exclusion Algorithm. - Kazuhiro Ogata 001; Kokichi Futatsugi (FMOODS, 2002)

Formal Analysis of the iKP Electronic Payment Protocols. - Kazuhiro Ogata 001; Kokichi Futatsugi (ISSS, 2002)

Rewriting-Based Verification of Authentication Protocols. - Kazuhiro Ogata 001; Kokichi Futatsugi (WRLA, 2002)

Proof Scores in the OTS/CafeOBJ Method. - Kazuhiro Ogata 001; Kokichi Futatsugi (FMOODS, 2003)

Formal Analysis of the NetBill Electronic Commerce Protocol. - Kazuhiro Ogata 001; Kokichi Futatsugi (ISSS, 2003)

Formal Verification of the Horn-Preneel Micropayment Protocol. - Kazuhiro Ogata 001; Kokichi Futatsugi (VMCAI, 2003)

CafeOBJ: Logical Foundations and Methodologies. - Razvan Diaconescu; Kokichi Futatsugi; Kazuhiro Ogata 001 (Comput. Artif. Intell., 2003)

Flaw and modification of the iKP electronic payment protocols. - Kazuhiro Ogata 001; Kokichi Futatsugi (Inf. Process. Lett., 2003)

Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol. - Weiqiang Kong; Kazuhiro Ogata 001; Jianwen Xiang; Kokichi Futatsugi (CIT, 2004)

Supporting Case Analysis with Algebraic Specification Languages. - Takahiro Seino; Kazuhiro Ogata 001; Kokichi Futatsugi (CIT, 2004)

Modeling and Verification of Hybrid Systems Based on Equations. - Kazuhiro Ogata 001; Daigo Yamagishi; Takahiro Seino; Kokichi Futatsugi (DIPES, 2004)

Equational Approach to Formal Verification of SET. - Kazuhiro Ogata 001; Kokichi Futatsugi (QSIC, 2004)

Analysis of the Suzuki-Kasami Algorithm with SAL Model Checkers. - Kazuhiro Ogata 001; Kokichi Futatsugi (CIT, 2005)

A Lightweight Integration of Theorem Proving and Model Checking for System Verification. - Weiqiang Kong; Takahiro Seino; Kokichi Futatsugi; Kazuhiro Ogata 001 (APSEC, 2005)

Analysis of the Suzuki-Kasami Algorithm with the Maude Model Checker. - Kazuhiro Ogata 001; Kokichi Futatsugi (APSEC, 2005)

Equational Approach to Formal Analysis of TLS. - Kazuhiro Ogata 001; Kokichi Futatsugi (ICDCS, 2005)

Chocolat/SMV: A Translator from CafeOBJ into SMV. - Kazuhiro Ogata 001; Masahiro Nakano; Masaki Nakamura 001; Kokichi Futatsugi (PDCAT, 2005)

Formal Fault Tree Analysis of State Transition Systems. - Jianwen Xiang; Kazuhiro Ogata 001 (QSIC, 2005)

Formal Analysis of Workflow Systems with Security Considerations. - Weiqiang Kong; Kazuhiro Ogata 001; Kokichi Futatsugi (SEKE, 2005)

Provably Correct Translation from CafeOBJ into Java. - Jittisak Senachak; Takahiro Seino; Kazuhiro Ogata 001; Kokichi Futatsugi (SEKE, 2005)

Verifying Design with Proof Scores. - Kokichi Futatsugi; Joseph A. Goguen; Kazuhiro Ogata 001 (VSTTE, 2005)

A Toolkit for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method. - Takahiro Seino; Kazuhiro Ogata 001; Kokichi Futatsugi (RULE@RDP, 2005)

Mechanically supporting case analysis for verification of distributed systems. - Takahiro Seino; Kazuhiro Ogata 001; Kokichi Futatsugi (Int. J. Pervasive Comput. Commun., 2005)

Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method. - Kazuhiro Ogata 001; Kokichi Futatsugi (Essays Dedicated to Joseph A. Goguen, 2006)

Induction-Guided Falsification. - Kazuhiro Ogata 001; Masahiro Nakano; Weiqiang Kong; Kokichi Futatsugi (ICFEM, 2006)

Automating Invariant Verification of Behavioral Specifications. - Masahiro Nakano; Kazuhiro Ogata 001; Masaki Nakamura 001; Kokichi Futatsugi (QSIC, 2006)

Falsification of OTSs by Searches of Bounded Reachable State Spaces. - Kazuhiro Ogata 001; Weiqiang Kong; Kokichi Futatsugi (SEKE, 2006)

Analysis of Positive Incentives for Protecting Secrets in Digital Rights Management. - Jianwen Xiang; Weiqiang Kong; Kokichi Futatsugi; Kazuhiro Ogata 001 (WEBIST (2), 2006)

Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System. - Weiqiang Kong; Kazuhiro Ogata 001; Kokichi Futatsugi (IFM, 2007)

Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method. - Kazuhiro Ogata 001; Kokichi Futatsugi (REFINE@IFM, 2007)

Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm. - Kazuhiro Ogata 001; Kokichi Futatsugi (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2007)

State Machines as Inductive Types. - Kazuhiro Ogata 001; Kokichi Futatsugi (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2007)

Specification and Verification of Workflows with Rbac Mechanism and Sod Constraints. - Weiqiang Kong; Kazuhiro Ogata 001; Kokichi Futatsugi (Int. J. Softw. Eng. Knowl. Eng., 2007)

CrÈme: an Automatic Invariant Prover of Behavioral Specifications. - Masahiro Nakano; Kazuhiro Ogata 001; Masaki Nakamura 001; Kokichi Futatsugi (Int. J. Softw. Eng. Knowl. Eng., 2007)

From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ. - Jianwen Xiang; Kazuhiro Ogata 001; Weiqiang Kong; Kokichi Futatsugi (Inf. Media Technol., 2007)

Modeling and verification of real-time systems based on equations. - Kazuhiro Ogata 001; Kokichi Futatsugi (Sci. Comput. Program., 2007)

Trace anonymity in the OTS/CafeOBJ method. - Weiqiang Kong; Kazuhiro Ogata 001; Jian Cheng; Kokichi Futatsugi (CIT, 2008)

Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes. - Kazuhiro Ogata 001; Kokichi Futatsugi (ICFEM, 2008)

A Specification Translation from Behavioral Specifications to Rewrite Specifications. - Masaki Nakamura 001; Weiqiang Kong; Kazuhiro Ogata 001; Kokichi Futatsugi (IEICE Trans. Inf. Syst., 2008)

Proof Score Approach to Verification of Liveness Properties. - Kazuhiro Ogata 001; Kokichi Futatsugi (IEICE Trans. Inf. Syst., 2008)

Constructor-Based Institutions. - Daniel Gâinâ; Kokichi Futatsugi; Kazuhiro Ogata 001 (CALCO, 2009)

Modular Implementation of a Translator from Behavioral Specifications to Rewrite Theory Specifications. - Min Zhang 002; Kazuhiro Ogata 001 (QSIC, 2009)

User-Defined On-Demand Matching. - Masaki Nakamura 001; Kazuhiro Ogata 001; Kokichi Futatsugi (IEICE Trans. Inf. Syst., 2009)

A Combination of Forward and Backward Reachability Analysis Methods. - Kazuhiro Ogata 001; Kokichi Futatsugi (ICFEM, 2010)

Specification Translation of State Machines from Equational Theories into Rewrite Theories. - Min Zhang 002; Kazuhiro Ogata 001; Masaki Nakamura 001 (ICFEM, 2010)

Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method. - Iakovos Ouranos; Petros S. Stefaneas; Kazuhiro Ogata 001 (ISoLA (1), 2010)

Towards Reliable E-Government Systems with the OTS/CafeOBJ Method. - Weiqiang Kong; Kazuhiro Ogata 001; Kokichi Futatsugi (IEICE Trans. Inf. Syst., 2010)

Proof Score Approach to Analysis of Electronic Commerce Protocols. - Kazuhiro Ogata 001; Kokichi Futatsugi (Int. J. Softw. Eng. Knowl. Eng., 2010)

Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications. - Masaki Nakamura 001; Kazuhiro Ogata 001; Kokichi Futatsugi (J. Symb. Comput., 2010)

Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support. - Min Zhang 002; Kazuhiro Ogata 001; Masaki Nakamura 001 (IEICE Trans. Inf. Syst., 2011)

Invariant-preserved Transformation of State Machines from Equations into Rewrite Rules. - Min Zhang 002; Kazuhiro Ogata 001 (APSEC, 2012)

An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms. - Min Zhang 002; Kazuhiro Ogata 001; Kokichi Futatsugi (APSEC, 2012)

Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic. - Kazuhiro Ogata 001; Thi Thanh Huyen Phan (ICFEM, 2012)

Formal Analysis of TESLA Protocol in the Timed OTS/CafeOBJ Method. - Iakovos Ouranos; Kazuhiro Ogata 001; Petros S. Stefaneas (ISoLA (2), 2012)

Constructor-based Logics. - Daniel Gâinâ; Kokichi Futatsugi; Kazuhiro Ogata 001 (J. Univers. Comput. Sci., 2012)

Principles of proof scores in CafeOBJ. - Kokichi Futatsugi; Daniel Gâinâ; Kazuhiro Ogata 001 (Theor. Comput. Sci., 2012)

Model Checking Liveness Properties under Fairness & Anti-fairness Assumptions. - Kazuhiro Ogata 001 (APSEC (1), 2013)

A Divide and Conquer Approach to Model Checking of Liveness Properties. - Kazuhiro Ogata 001; Min Zhang 002 (COMPSAC, 2013)

Formalization and Verification of Behavioral Correctness of Dynamic Software Updates. - Min Zhang 002; Kazuhiro Ogata 001; Kokichi Futatsugi (VSSE, 2013)

Foreword. - Kazuhiro Ogata 001 (IEICE Trans. Inf. Syst., 2013)

Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method. - Kazuhiro Ogata 001; Kokichi Futatsugi (J. Univers. Comput. Sci., 2013)

Evaluation of Maude as a Test Generation Engine for Automotive Operating Systems. - Yunja Choi; Min Zhang 002; Kazuhiro Ogata 001 (APSEC (1), 2014)

Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method. - Min Zhang 002; Kazuhiro Ogata 001; Kokichi Futatsugi (Specification, Algebra, and Software, 2014)

On Automation of OTS/CafeOBJ Method. - Daniel Gâinâ; Dorel Lucanu; Kazuhiro Ogata 001; Kokichi Futatsugi (Specification, Algebra, and Software, 2014)

Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications. - Masaki Nakamura 001; Kazuhiro Ogata 001; Kokichi Futatsugi (Specification, Algebra, and Software, 2014)

Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs. - Kazuhiro Ogata 001; Kokichi Futatsugi (Specification, Algebra, and Software, 2014)

Liveness Properties in CafeOBJ - A Case Study for Meta-Level Specifications. - Norbert Preining; Kazuhiro Ogata 001; Kokichi Futatsugi (LOPSTR, 2014)

A Formal Semantics of the OSEK/VDX Standard in $${ mathbb {K}}$$ Framework and Its Applications. - Min Zhang 002; Yunja Choi; Kazuhiro Ogata 001 (WRLA, 2014)

TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned. - Iakovos Ouranos; Kazuhiro Ogata 001; Petros S. Stefaneas (IEICE Trans. Inf. Syst., 2014)

Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates. - Min Zhang 002; Kazuhiro Ogata 001; Kokichi Futatsugi (APSEC, 2015)

Proving Sufficient Completeness of Constructor-Based Algebraic Specifications. - Masaki Nakamura 001; Daniel Gâinâ; Kazuhiro Ogata 001; Kokichi Futatsugi (CSA/CUTE, 2015)

Formalization and Verification of Declarative Cloud Orchestration. - Hiroyuki Yoshida; Kazuhiro Ogata 001; Kokichi Futatsugi (ICFEM, 2015)

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 002; Kazuhiro Ogata 001 (ILP (Late Breaking Papers), 2015)

CafeInMaude: A CafeOBJ Interpreter in Maude. - Adrián Riesco 001; Kazuhiro Ogata 001; Kokichi Futatsugi (FASE, 2016)

Model Checking of a Mobile Robots Perpetual Exploration Algorithm. - Ha Thi Thu Doan; François Bonnet 001; Kazuhiro Ogata 001 (SOFL+MSVL, 2016)

Formal modeling and analysis of time- and resource-sensitive simple business processes. - Kazuhiro Ogata 001; Thapana Chaimanont; Min Zhang 002 (J. Inf. Secur. Appl., 2016)

Writing Concurrent Java Programs Based on CafeOBJ Specifications. - Xuan-Linh Ha; Kazuhiro Ogata 001 (APSEC, 2017)

Graphical Animations of State Machines. - Tam Thi Thanh Nguyen; Kazuhiro Ogata 001 (DASC/PiCom/DataCom/CyberSciTech, 2017)

Specifying a Distributed Snapshot Algorithm as a Meta-Program and Model Checking it at Meta-Level. - Ha Thi Thu Doan; Kazuhiro Ogata 001; François Bonnet 001 (ICDCS, 2017)

A Formal Proof Generator from Semi-formal Proof Documents. - Adrián Riesco 001; Kazuhiro Ogata 001 (ICTAC, 2017)

Model Checking of Robot Gathering. - Ha Thi Thu Doan; François Bonnet 001; Kazuhiro Ogata 001 (OPODIS, 2017)

A Way to Comprehend Counterexamples Generated by the Maude LTL Model Checker. - Tam Thi Thanh Nguyen; Kazuhiro Ogata 001 (SATE, 2017)

A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler. - Dorian Daudier; Trinh Ngoc Quoc Bao; Kazuhiro Ogata 001 (SOFL+MSVL, 2017)

Graphically Perceiving Characteristics of the MCS Lock and Model Checking Them. - Tam Thi Thanh Nguyen; Kazuhiro Ogata 001 (SOFL+MSVL, 2017)

A Maude environment for CafeOBJ. - Adrián Riesco 001; Kazuhiro Ogata 001; Kokichi Futatsugi (Formal Aspects Comput., 2017)

Model checking the iKP electronic payment protocols. - Kazuhiro Ogata 001 (J. Inf. Secur. Appl., 2017)

Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks. - Yati Phyo; Kazuhiro Ogata 001 (APSEC, 2018)

Analysis of Some Variants of the Anderson Array-Based Queuing Mutual Exclusion Protocol with Model Checking and Graphical Animations. - Yati Phyo; Kazuhiro Ogata 001 (DSA, 2018)

Model Checking of the Suzuki-Kasami Distributed Mutual Exclusion Algorithm with SPIN. - Shouki Sakamoto; Kazuhiro Ogata 001 (DSA, 2018)

Guessing Properties of the Qlock Mutual Exclusion Protocol based on its Graphical Animations and confirming the Properties by Model Checking. - May Thu Aung; Tam Thi Thanh Nguyen; Kazuhiro Ogata 001 (ICSCA, 2018)

Analysis of Two Flawed Versions of A Mutual Exclusion Protocol with Maude and SMGA. - May Thu Aung; Tam Thi Thanh Nguyen; Kazuhiro Ogata 001 (ICSCA, 2018)

Formal analysis of a security protocol for e-passports based on rewrite theory specifications. - Manjukeshwar Reddy Mandadi; Varuneshwar Reddy Mandadi; Kazuhiro Ogata 001 (J. Inf. Secur. Appl., 2018)

From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories. - Min Zhang 002; Kazuhiro Ogata 001 (Theor. Comput. Sci., 2018)

Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores. - Adrián Riesco 001; Kazuhiro Ogata 001 (ACM Trans. Softw. Eng. Methodol., 2018)

KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs. - Jiaqi Qian; Min Zhang 002; Yi Wang 013; Kazuhiro Ogata 001 (FASE, 2019)

Formal Specification and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S). - Moe Nandi Aung; Yati Phyo; Kazuhiro Ogata 001 (SEKE, 2019)

Specification-based Testing with Simulation Relations (S). - Canh Minh Do; Kazuhiro Ogata 001 (SEKE, 2019)

Formal Specification and Model Checking of A* Algorithm. - Kazuhiro Ogata 001 (SEKE, 2019)

A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and Maude. - Canh Minh Do; Kazuhiro Ogata 001 (SOFL+MSVL, 2019)

Formal Specification and Model Checking of a Ride-sharing System in Maude. - Eiichi Muramoto; Kazuhiro Ogata 001; Yoichi Shinoda (SOFL+MSVL, 2019)

An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms. - Ha Thi Thu Doan; Adrián Riesco 001; Kazuhiro Ogata 001 (SSS, 2019)

A More Faithful Formal Definition of the Desired Property for Distributed Snapshot Algorithms to Model Check the Property. - Ha Thi Thu Doan; Kazuhiro Ogata 001 (Comput. Informatics, 2019)

A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions. - Kazuhiro Ogata 001 (Frontiers Comput. Sci., 2019)

Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol. - Dang Duy Bui; Kazuhiro Ogata 001 (J. Vis. Lang. Comput., 2019)

A divide & conquer approach to testing concurrent programs with JPF*. - Canh Minh Do; Kazuhiro Ogata 001 (APSEC, 2020)

Lemma Weakening for State Machine Invariant Proofs. - Duong Dinh Tran; Dang Duy Bui; Parth Gupta; Kazuhiro Ogata 001 (APSEC, 2020)

CiMPG+F: A Proof Generator and Fixer-Upper for CafeOBJ Specifications. - Adrián Riesco 001; Kazuhiro Ogata 001 (ICTAC, 2020)

Parallel stratified random testing for concurrent programs. - Canh Minh Do; Kazuhiro Ogata 001 (QRS Companion, 2020)

Formal verification of an abstract version of Anderson protocol with CafeOBJ, CiMPA and CiMPG. - Duong Dinh Tran; Kazuhiro Ogata 001 (SEKE, 2020)

Formal verification of Fischer's real-time mutual exclusion protocol by the OTS/CafeOBJ method. - Masaki Nakamura 001; Shuki Higashi; Kazutoshi Sakakibara; Kazuhiro Ogata 001 (SICE, 2020)

Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method. - Masaki Nakamura 001; Kazutoshi Sakakibara; Kazuhiro Ogata 001 (CoRR, 2020)

A Generic Approach on How to Formally Specify and Model Check Path Finding Algorithms: Dijkstra, A* and LPA. - Kazuhiro Ogata 001 (Int. J. Softw. Eng. Knowl. Eng., 2020)

Formal analysis of RFC 8120 authentication protocol for HTTP under different assumptions. - Naomi Okumura; Kazuhiro Ogata 001; Yoichi Shinoda (J. Inf. Secur. Appl., 2020)

Stability of termination and sufficient-completeness under pushouts via amalgamation. - Daniel Gaina; Masaki Nakamura 001; Kazuhiro Ogata 001; Kokichi Futatsugi (Theor. Comput. Sci., 2020)

A support tool for the L + 1-layer divide & conquer approach to leads-to model checking. - Yati Phyo; Canh Minh Do; Kazuhiro Ogata 001 (COMPSAC, 2021)

Graphical Animations of the NSLPK Authentication Protocol (S). - Thet Wai Mon; Dang Duy Bui; Duong Dinh Tran; Kazuhiro Ogata 001 (DMSVIVA, 2021)

Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S). - Win Hlaing Hlaing Myint; Dang Duy Bui; Duong Dinh Tran; Kazuhiro Ogata 001 (DMSVIVA, 2021)

A Divide & Conquer Approach to Conditional Stable Model Checking. - Yati Phyo; Canh Minh Do; Kazuhiro Ogata 001 (ICTAC, 2021)

Formal Specification and Model Checking of an Autonomous Vehicle Merging Protocol. - Minxuan Liu; Dang Duy Bui; Duong Dinh Tran; Kazuhiro Ogata 001 (QRS Companion, 2021)

Formal verification of Anderson mutual exclusion protocol by introducing an auxiliary variable (S). - Naoki Asae; Duong Dinh Tran; Kazuhiro Ogata 001 (SEKE, 2021)

Formal verification of IFF and NSLPK authentication protocols with CiMPG (S). - Thet Wai Mon; Shuho Fujii; Duong Dinh Tran; Kazuhiro Ogata 001 (SEKE, 2021)

Formal specification and model checking of a recoverable wait-free version of MCS. - Duong Dinh Tran; Kentaro Waki; Kazuhiro Ogata 001 (SEKE, 2021)

Simulation-Based Invariant Verification Technique for the OTS/CafeOBJ Method. - Duong Dinh Tran; Dang Duy Bui; Kazuhiro Ogata 001 (IEEE Access, 2021)

Formal Verification of Multitask Hybrid Systems by the OTS/CafeOBJ Method. - Masaki Nakamura 001; Kazutoshi Sakakibara; Yuki Okura; Kazuhiro Ogata 001 (Int. J. Softw. Eng. Knowl. Eng., 2021)

Graphical Animations of the NS(L)PK Authentication Protocols. - Thet Wai Mon; Dang Duy Bui; Duong Dinh Tran; Canh Minh Do; Kazuhiro Ogata 001 (J. Vis. Lang. Comput., 2021)

IPSG: Invariant Proof Score Generator. - Duong Dinh Tran; Kazuhiro Ogata 001 (COMPSAC, 2022)

Graphical Animations of an Autonomous Vehicle Merging Protocol. - Minxuan Liu; Kazuhiro Ogata 001; Dang Duy Bui (DMSVIVA, 2022)

Integration of SMGA and Maude to Facilitate Characteristic Conjecture. - Dang Duy Bui; Duong Dinh Tran; Kazuhiro Ogata 001; Adrián Riesco 001 (DMSVIVA, 2022)

A Tool for Model Checking Eventual Model Checking in a Stratified Way. - Moe Nandi Aung; Yati Phyo; Canh Minh Do; Kazuhiro Ogata 001 (DSA, 2022)

Modeling and verification of the post-quantum key encapsulation mechanism KYBER using Maude. - Víctor García; Santiago Escobar 001; Kazuhiro Ogata 001 (FAVPQC@ICFEM, 2022)

Formal specification and model checking of lattice-based key encapsulation mechanisms in Maude. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (FAVPQC@ICFEM, 2022)

Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security analysis. - Duong Dinh Tran; Canh Minh Do; Santiago Escobar 001; Kazuhiro Ogata 001 (FAVPQC@ICFEM, 2022)

A divide and conquer approach to until and until stable model checking. - Canh Minh Do; Yati Phyo; Kazuhiro Ogata 001 (SEKE, 2022)

Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (SEKE, 2022)

Parallel Maude-NPA for Cryptographic Protocol Analysis. - Canh Minh Do; Adrián Riesco 001; Santiago Escobar 001; Kazuhiro Ogata 001 (WRLA@ETAPS, 2022)

Parallel Specification-Based Testing for Concurrent Programs. - Canh Minh Do; Kazuhiro Ogata 001 (IEEE Access, 2022)

Sequential and Parallel Tools for Model Checking Conditional Stable Properties in a Layered Way. - Canh Minh Do; Yati Phyo; Kazuhiro Ogata 001 (IEEE Access, 2022)

Specifying and Model Checking Distributed Control Algorithms at Meta-level. - Ha Thi Thu Doan; Kazuhiro Ogata 001 (Comput. J., 2022)

A Divide & Conquer Approach to Leads-to Model Checking. - Yati Phyo; Canh Minh Do; Kazuhiro Ogata 001 (Comput. J., 2022)

Formal verification of TLS 1.2 by automatically generating proof scores. - Duong Dinh Tran; Kazuhiro Ogata 001 (Comput. Secur., 2022)

Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method. - Masaki Nakamura 001; Shuki Higashi; Kazutoshi Sakakibara; Kazuhiro Ogata 001 (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2022)

An integrated tool set for verifying CafeOBJ specifications. - Adrián Riesco 001; Kazuhiro Ogata 001 (J. Syst. Softw., 2022)

Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol. - Dang Duy Bui; Win Hlaing Hlaing Myint; Duong Dinh Tran; Kazuhiro Ogata 001 (J. Vis. Lang. Comput., 2022)

Better state pictures facilitating state machine characteristic conjecture. - Dang Duy Bui; Kazuhiro Ogata 001 (Multim. Tools Appl., 2022)

Automated Quantum Program Verification in Dynamic Quantum Logic. - Tsubasa Takagi; Canh Minh Do; Kazuhiro Ogata 001 (DaLí, 2023)

Formal Specification and Model Checking of Raft Log Replication in Maude. - Takanori Ishibashi; Kazuhiro Ogata 001 (DMSVIVA, 2023)

Formal Specification and Model Checking of Raft Leader Election in Maude. - Takanori Ishibashi; Kazuhiro Ogata 001 (ICSCA, 2023)

A way to find counterexamples located at deep positions with domain knowledge of authentication protocols. - Naomi Okumura; Kazuhiro Ogata 001 (ICSCA, 2023)

Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (IET Inf. Secur., 2023)

A Layered and Parallelized Method of Eventual Model Checking. - Yati Phyo; Moe Nandi Aung; Canh Minh Do; Kazuhiro Ogata 001 (Inf., 2023)

Graphical Animations of an Autonomous Vehicle Merging Protocol. - Dang Duy Bui; Minxuan Liu; Duong Ding Tran; Kazuhiro Ogata 001 (J. Vis. Lang. Comput., 2023)

Modelling and verification of post-quantum key encapsulation mechanisms using Maude. - Víctor García; Santiago Escobar 001; Kazuhiro Ogata 001; Sedat Akleylek; Ayoub Otmani (PeerJ Comput. Sci., 2023)

Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version. - Duong Dinh Tran; Canh Minh Do; Santiago Escobar 001; Kazuhiro Ogata 001 (PeerJ Comput. Sci., 2023)

Transport Layer Security 1.0 handshake protocol formal verification case study: How to use a proof script generator for existing large proof scores. - Duong Dinh Tran; Thet Wai Mon; Kazuhiro Ogata 001 (PeerJ Comput. Sci., 2023)

Selected papers from the 15th international symposium on Theoretical Aspects of Software Engineering (TASE 2021). - Min Zhang 002; Kazuhiro Ogata 001 (Sci. Comput. Program., 2023)

Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way. - Canh Minh Do; Yati Phyo; Adrián Riesco 001; Kazuhiro Ogata 001 (ACM Trans. Softw. Eng. Methodol., 2023)

A Tableau-Based Approach to Model Checking Linear Temporal Properties. - Canh Minh Do; Tsubasa Takagi; Kazuhiro Ogata 001 (ICFEM, 2024)

An Executable Operational Semantics of Quantum Programs and Its Application. - Canh Minh Do; Kazuhiro Ogata 001 (SFPVV, 2024)

Formal Specification and Model Checking of a Synchronous Leader Election Protocol in Maude. - Tomoyoshi Ogura; Canh Minh Do; Kazuhiro Ogata 001 (SFPVV, 2024)

Equivalence Checking of Quantum Circuits Based on Dirac Notation in Maude. - Canh Minh Do; Kazuhiro Ogata 001 (WRLA, 2024)

Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ. - Duong Dinh Tran; Kazuhiro Ogata 001 (WRLA, 2024)

Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer Protocol. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (IEEE Access, 2024)

Symbolic model checking quantum circuits in Maude. - Canh Minh Do; Kazuhiro Ogata 001 (PeerJ Comput. Sci., 2024)

Integration of state machine graphical animation and Maude to facilitate characteristic conjecture: an approach to lemma discovery in theorem proving. - Dang Duy Bui; Duong Dinh Tran; Kazuhiro Ogata 001; Adrián Riesco 001 (Multim. Tools Appl., 2024)

Formalization and analysis of the post-quantum signature scheme FALCON with Maude. - Víctor García; Santiago Escobar 001; Kazuhiro Ogata 001 (J. Log. Algebraic Methods Program., 2025)

Proof Scores: A Survey (full version). - Adrián Riesco 001; Kazuhiro Ogata 001; Masaki Nakamura 001; Daniel Gaina; Duong Dinh Tran; Kokichi Futatsugi (CoRR, 2025)

Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic. - Canh Minh Do; Tsubasa Takagi; Kazuhiro Ogata 001 (ACM Trans. Softw. Eng. Methodol., 2025)

Proof Scores: A Survey. - Adrián Riesco 001; Kazuhiro Ogata 001; Masaki Nakamura 001; Daniel Gaina; Duong Dinh Tran; Kokichi Futatsugi (ACM Comput. Surv., 2025)