Kazuhiro Ogata

ORCID

Publication Activity (10 Years)

Years Active: 1992-2024
Publications (10 Years): 95

Top Venues

Publications

Canh Minh Do, Kazuhiro Ogata
Symbolic model checking quantum circuits in Maude. PeerJ Comput. Sci. 10 (2024)
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani
Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer Protocol. IEEE Access 12 (2024)
Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata, Adrián Riesco
Integration of state machine graphical animation and Maude to facilitate characteristic conjecture: an approach to lemma discovery in theorem proving. Multim. Tools Appl. 83 (12) (2024)
Canh Minh Do, Kazuhiro Ogata
Equivalence Checking of Quantum Circuits Based on Dirac Notation in Maude. WRLA (2024)
Duong Dinh Tran, Kazuhiro Ogata
Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ. WRLA (2024)
Min Zhang, Kazuhiro Ogata
Selected papers from the 15th international symposium on Theoretical Aspects of Software Engineering (TASE 2021). Sci. Comput. Program. 225 (2023)
Duong Dinh Tran, Thet Wai Mon, Kazuhiro Ogata
Transport Layer Security 1.0 handshake protocol formal verification case study: How to use a proof script generator for existing large proof scores. PeerJ Comput. Sci. 9 (2023)
Duong Dinh Tran, Canh Minh Do, Santiago Escobar, Kazuhiro Ogata
Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version. PeerJ Comput. Sci. 9 (2023)
Yati Phyo, Moe Nandi Aung, Canh Minh Do, Kazuhiro Ogata
A Layered and Parallelized Method of Eventual Model Checking. Inf. 14 (7) (2023)
Dang Duy Bui, Minxuan Liu, Duong Ding Tran, Kazuhiro Ogata
Graphical Animations of an Autonomous Vehicle Merging Protocol. J. Vis. Lang. Comput. 2023 (1) (2023)
Takanori Ishibashi, Kazuhiro Ogata
Formal Specification and Model Checking of Raft Leader Election in Maude. ICSCA (2023)
Takanori Ishibashi, Kazuhiro Ogata
Formal Specification and Model Checking of Raft Log Replication in Maude. DMSVIVA (2023)
Canh Minh Do, Kazuhiro Ogata
Symbolic Model Checking Quantum Circuits in Maude. SEKE (2023)
Víctor García, Santiago Escobar, Kazuhiro Ogata, Sedat Akleylek, Ayoub Otmani
Modelling and verification of post-quantum key encapsulation mechanisms using Maude. PeerJ Comput. Sci. 9 (2023)
Canh Minh Do, Yati Phyo, Adrián Riesco, Kazuhiro Ogata
Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way. ACM Trans. Softw. Eng. Methodol. 32 (6) (2023)
Tsubasa Takagi, Canh Minh Do, Kazuhiro Ogata
Automated Quantum Program Verification in Dynamic Quantum Logic. DaLí (2023)
Naomi Okumura, Kazuhiro Ogata
A way to find counterexamples located at deep positions with domain knowledge of authentication protocols. ICSCA (2023)
Canh Minh Do, Yati Phyo, Kazuhiro Ogata
A divide and conquer approach to until and until stable model checking. SEKE (2022)
Masaki Nakamura, Shuki Higashi, Kazutoshi Sakakibara, Kazuhiro Ogata
Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. (5) (2022)
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani
Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude. SEKE (2022)
Adrián Riesco, Kazuhiro Ogata
An integrated tool set for verifying CafeOBJ specifications. J. Syst. Softw. 189 (2022)
Dang Duy Bui, Win Hlaing Hlaing Myint, Duong Dinh Tran, Kazuhiro Ogata
Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol. J. Vis. Lang. Comput. 2022 (1) (2022)
Moe Nandi Aung, Yati Phyo, Canh Minh Do, Kazuhiro Ogata
A Tool for Model Checking Eventual Model Checking in a Stratified Way. DSA (2022)
Minxuan Liu, Kazuhiro Ogata, Dang Duy Bui
Graphical Animations of an Autonomous Vehicle Merging Protocol. DMSVIVA (2022)
Canh Minh Do, Kazuhiro Ogata
Parallel Specification-Based Testing for Concurrent Programs. IEEE Access 10 (2022)
Ha Thi Thu Doan, Kazuhiro Ogata
Specifying and Model Checking Distributed Control Algorithms at Meta-level. Comput. J. 65 (12) (2022)
Canh Minh Do, Adrián Riesco, Santiago Escobar, Kazuhiro Ogata
Parallel Maude-NPA for Cryptographic Protocol Analysis. WRLA@ETAPS (2022)
Yati Phyo, Canh Minh Do, Kazuhiro Ogata
A Divide & Conquer Approach to Leads-to Model Checking. Comput. J. 65 (6) (2022)
Duong Dinh Tran, Kazuhiro Ogata
Formal verification of TLS 1.2 by automatically generating proof scores. Comput. Secur. 123 (2022)
Duong Dinh Tran, Canh Minh Do, Santiago Escobar, Kazuhiro Ogata
Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security analysis. FAVPQC@ICFEM (2022)
Víctor García, Santiago Escobar, Kazuhiro Ogata
Modeling and verification of the post-quantum key encapsulation mechanism KYBER using Maude. FAVPQC@ICFEM (2022)
Duong Dinh Tran, Kazuhiro Ogata
IPSG: Invariant Proof Score Generator. COMPSAC (2022)
Duong Dinh Tran, Kazuhiro Ogata, Adrián Riesco, Dang Duy Bui
Integration of SMGA and Maude to Facilitate Characteristic Conjecture. DMSVIVA (2022)
Dang Duy Bui, Kazuhiro Ogata
Better state pictures facilitating state machine characteristic conjecture. Multim. Tools Appl. 81 (1) (2022)
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani
Formal specification and model checking of lattice-based key encapsulation mechanisms in Maude. FAVPQC@ICFEM (2022)
Canh Minh Do, Yati Phyo, Kazuhiro Ogata
Sequential and Parallel Tools for Model Checking Conditional Stable Properties in a Layered Way. IEEE Access 10 (2022)
Masaki Nakamura, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata
Formal Verification of Multitask Hybrid Systems by the OTS/CafeOBJ Method. Int. J. Softw. Eng. Knowl. Eng. 31 (11&12) (2021)
Minxuan Liu, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata
Formal Specification and Model Checking of an Autonomous Vehicle Merging Protocol. QRS Companion (2021)
Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, Canh Minh Do, Kazuhiro Ogata
Graphical Animations of the NS(L)PK Authentication Protocols. J. Vis. Lang. Comput. 2021 (2) (2021)
Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata
Graphical Animations of the NSLPK Authentication Protocol (S). DMSVIVA (2021)
Thet Wai Mon, Shuho Fujii, Duong Dinh Tran, Kazuhiro Ogata
Formal verification of IFF and NSLPK authentication protocols with CiMPG (S). SEKE (2021)
Duong Dinh Tran, Dang Duy Bui, Kazuhiro Ogata
Simulation-Based Invariant Verification Technique for the OTS/CafeOBJ Method. IEEE Access 9 (2021)
Masaki Nakamura, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata
Formal verification of multitask hybrid systems by the OTS/CafeOBJ method. SEKE (2021)
Duong Dinh Tran, Kentaro Waki, Kazuhiro Ogata
Formal specification and model checking of a recoverable wait-free version of MCS. SEKE (2021)
Win Hlaing Hlaing Myint, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata
Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S). DMSVIVA (2021)
Yati Phyo, Canh Minh Do, Kazuhiro Ogata
A Divide & Conquer Approach to Conditional Stable Model Checking. ICTAC (2021)
Yati Phyo, Canh Minh Do, Kazuhiro Ogata
A support tool for the L + 1-layer divide & conquer approach to leads-to model checking. COMPSAC (2021)
Naoki Asae, Duong Dinh Tran, Kazuhiro Ogata
Formal verification of Anderson mutual exclusion protocol by introducing an auxiliary variable (S). SEKE (2021)
Kazuhiro Ogata
A Generic Approach on How to Formally Specify and Model Check Path Finding Algorithms: Dijkstra, A* and LPA. Int. J. Softw. Eng. Knowl. Eng. 30 (10) (2020)
Masaki Nakamura, Shuki Higashi, Kazutoshi Sakakibara, Kazuhiro Ogata
Formal verification of Fischer's real-time mutual exclusion protocol by the OTS/CafeOBJ method. SICE (2020)
Duong Dinh Tran, Dang Duy Bui, Parth Gupta, Kazuhiro Ogata
Lemma Weakening for State Machine Invariant Proofs. APSEC (2020)
Naomi Okumura, Kazuhiro Ogata, Yoichi Shinoda
Formal analysis of RFC 8120 authentication protocol for HTTP under different assumptions. J. Inf. Secur. Appl. 53 (2020)
Dang Duy Bui, Kazuhiro Ogata
Better State Pictures Facilitating State Machine Characteristic Conjecture. DMSVIVA (2020)
Duong Dinh Tran, Kazuhiro Ogata
Formal verification of an abstract version of Anderson protocol with CafeOBJ, CiMPA and CiMPG. SEKE (2020)
Canh Minh Do, Kazuhiro Ogata
Parallel stratified random testing for concurrent programs. QRS Companion (2020)
Canh Minh Do, Kazuhiro Ogata
. APSEC (2020)
Masaki Nakamura, Kazutoshi Sakakibara, Kazuhiro Ogata
Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method. CoRR (2020)
Adrián Riesco, Kazuhiro Ogata
CiMPG+F: A Proof Generator and Fixer-Upper for CafeOBJ Specifications. ICTAC (2020)
Daniel Gaina, Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
Stability of termination and sufficient-completeness under pushouts via amalgamation. Theor. Comput. Sci. 848 (2020)
Eiichi Muramoto, Kazuhiro Ogata, Yoichi Shinoda
Formal Specification and Model Checking of a Ride-sharing System in Maude. SOFL+MSVL (2019)
Ha Thi Thu Doan, Adrián Riesco, Kazuhiro Ogata
An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms. SSS (2019)
Canh Minh Do, Kazuhiro Ogata
A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and Maude. SOFL+MSVL (2019)
Dang Duy Bui, Kazuhiro Ogata
Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol. J. Vis. Lang. Comput. 2019 (2) (2019)
Canh Minh Do, Kazuhiro Ogata
Specification-based Testing with Simulation Relations (S). SEKE (2019)
Kazuhiro Ogata
A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions. Frontiers Comput. Sci. 13 (1) (2019)
Ha Thi Thu Doan, Kazuhiro Ogata
A More Faithful Formal Definition of the Desired Property for Distributed Snapshot Algorithms to Model Check the Property. Comput. Informatics 38 (5) (2019)
Moe Nandi Aung, Yati Phyo, Kazuhiro Ogata
Formal Specification and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S). SEKE (2019)
Dang Duy Bui, Kazuhiro Ogata
Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol. DMSVIVA (2019)
Kazuhiro Ogata
Formal Specification and Model Checking of A* Algorithm. SEKE (2019)
Jiaqi Qian, Min Zhang, Yi Wang, Kazuhiro Ogata
KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs. FASE (2019)
Manjukeshwar Reddy Mandadi, Varuneshwar Reddy Mandadi, Kazuhiro Ogata
Formal analysis of a security protocol for e-passports based on rewrite theory specifications. J. Inf. Secur. Appl. 42 (2018)
Adrián Riesco, Kazuhiro Ogata
Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores. ACM Trans. Softw. Eng. Methodol. 27 (2) (2018)
Shouki Sakamoto, Kazuhiro Ogata
Model Checking of the Suzuki-Kasami Distributed Mutual Exclusion Algorithm with SPIN. DSA (2018)
Yati Phyo, Kazuhiro Ogata
Analysis of Some Variants of the Anderson Array-Based Queuing Mutual Exclusion Protocol with Model Checking and Graphical Animations. DSA (2018)
May Thu Aung, Tam Thi Thanh Nguyen, Kazuhiro Ogata
Analysis of Two Flawed Versions of A Mutual Exclusion Protocol with Maude and SMGA. ICSCA (2018)
Min Zhang, Kazuhiro Ogata
From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories. Theor. Comput. Sci. 722 (2018)
Yati Phyo, Kazuhiro Ogata
Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks. APSEC (2018)
May Thu Aung, Tam Thi Thanh Nguyen, Kazuhiro Ogata
Guessing Properties of the Qlock Mutual Exclusion Protocol based on its Graphical Animations and confirming the Properties by Model Checking. ICSCA (2018)
Ha Thi Thu Doan, François Bonnet, Kazuhiro Ogata
Model Checking of Robot Gathering. OPODIS (2017)
Ha Thi Thu Doan, Kazuhiro Ogata, François Bonnet
Specifying a Distributed Snapshot Algorithm as a Meta-Program and Model Checking it at Meta-Level. ICDCS (2017)
Xuan-Linh Ha, Kazuhiro Ogata
Writing Concurrent Java Programs Based on CafeOBJ Specifications. APSEC (2017)
Tam Thi Thanh Nguyen, Kazuhiro Ogata
Graphically Perceiving Characteristics of the MCS Lock and Model Checking Them. SOFL+MSVL (2017)
Tam Thi Thanh Nguyen, Kazuhiro Ogata
A Way to Comprehend Counterexamples Generated by the Maude LTL Model Checker. SATE (2017)
Tam Thi Thanh Nguyen, Kazuhiro Ogata
Graphical Animations of State Machines. DASC/PiCom/DataCom/CyberSciTech (2017)
Kazuhiro Ogata
Model checking the iKP electronic payment protocols. J. Inf. Secur. Appl. 36 (2017)
Dorian Daudier, Trinh Ngoc Quoc Bao, Kazuhiro Ogata
A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler. SOFL+MSVL (2017)
Adrián Riesco, Kazuhiro Ogata
A Formal Proof Generator from Semi-formal Proof Documents. ICTAC (2017)
Adrián Riesco, Kazuhiro Ogata, Kokichi Futatsugi
A Maude environment for CafeOBJ. Formal Aspects Comput. 29 (2) (2017)
Adrián Riesco, Kazuhiro Ogata, Kokichi Futatsugi
CafeInMaude: A CafeOBJ Interpreter in Maude. FASE (2016)
Ha Thi Thu Doan, François Bonnet, Kazuhiro Ogata
Model Checking of a Mobile Robots Perpetual Exploration Algorithm. SOFL+MSVL (2016)
Kazuhiro Ogata, Thapana Chaimanont, Min Zhang
Formal modeling and analysis of time- and resource-sensitive simple business processes. J. Inf. Secur. Appl. 31 (2016)
Masaki Nakamura, Daniel Gâinâ, Kazuhiro Ogata, Kokichi Futatsugi
Proving Sufficient Completeness of Constructor-Based Algebraic Specifications. CSA/CUTE (2015)
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates. APSEC (2015)
Hiroyuki Yoshida, Kazuhiro Ogata, Kokichi Futatsugi
Formalization and Verification of Declarative Cloud Orchestration. ICFEM (2015)
Dung Tuan Ho, Min Zhang, Kazuhiro Ogata
Case Studies on Extracting the Characteristics of the Reachable States of State Machines Formalizing Communication Protocols with Inductive Logic Programing. ILP (Late Breaking Papers) (2015)
Yunja Choi, Min Zhang, Kazuhiro Ogata
Evaluation of Maude as a Test Generation Engine for Automotive Operating Systems. APSEC (1) (2014)
Kazuhiro Ogata, Kokichi Futatsugi
Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs. Specification, Algebra, and Software (2014)
Iakovos Ouranos, Kazuhiro Ogata, Petros S. Stefaneas
TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned. IEICE Trans. Inf. Syst. (5) (2014)
Min Zhang, Yunja Choi, Kazuhiro Ogata
A Formal Semantics of the OSEK/VDX Standard in $${\mathbb {K}}$$ Framework and Its Applications. WRLA (2014)
Daniel Gâinâ, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi
On Automation of OTS/CafeOBJ Method. Specification, Algebra, and Software (2014)

Kazuhiro Ogata.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Kazuhiro Ogata