Kazuhiro Ogata

198 papers A* 2A 3B 9C 46Misc 2Journal 62Unranked 71

Year	Rank	Type	Title / Venue / Authors
2025	—	`conf`	A Support Tool for Verification of Simulation Relations Between State Machines with Maude. SFPVV Takanori Ishibashi, Masaki Nakamura, Kazuhiro Ogata
2025	J	`jnl`	Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic. ACM Trans. Softw. Eng. Methodol. Canh Minh Do, Tsubasa Takagi, Kazuhiro Ogata
2025	C	`conf`	Folding Narrowing for the Analysis of Mutual Exclusion Protocols. PPDP Raúl López-Rueda, Duong Dinh Tran, Canh Minh Do, Santiago Escobar, Kazuhiro Ogata
2025	C	`conf`	Formal Specification and Analysis of Post-quantum OpenPGP Protocol in CafeOBJ. SEKE Trong Binh Hoang, Duong Dinh Tran, Canh Minh Do, Kazuhiro Ogata
2025	C	`conf`	Formal Specification and Model Checking of the BB84 Protocol in Maude (S). SEKE Canh Minh Do, Kazuhiro Ogata
2025	J	`jnl`	Formalization and analysis of the post-quantum signature scheme FALCON with Maude. J. Log. Algebraic Methods Program. Víctor García, Santiago Escobar, Kazuhiro Ogata
2025	J	`jnl`	Parallel Maude-NPA for Cryptographic Protocol Analysis. IEEE Trans. Dependable Secur. Comput. Canh Minh Do, Adrián Riesco, Santiago Escobar, Kazuhiro Ogata
2025	J	`jnl`	Proof Scores: A Survey (full version). CoRR Adrián Riesco, Kazuhiro Ogata, Masaki Nakamura, Daniel Gaina, Duong Dinh Tran, Kokichi Futatsugi
2025	J	`jnl`	Proof Scores: A Survey. ACM Comput. Surv. Adrián Riesco, Kazuhiro Ogata, Masaki Nakamura, Daniel Gaina, Duong Dinh Tran, Kokichi Futatsugi
2025	—	`conf`	QRAT: A Reachability Analysis Tool for Quantum Programs. SFPVV Canh Minh Do, Kazuhiro Ogata
2024	C	`conf`	A Tableau-Based Approach to Model Checking Linear Temporal Properties. ICFEM Canh Minh Do, Tsubasa Takagi, Kazuhiro Ogata
2024	—	`conf`	An Executable Operational Semantics of Quantum Programs and Its Application. SFPVV Canh Minh Do, Kazuhiro Ogata
2024	—	`conf`	Equivalence Checking of Quantum Circuits Based on Dirac Notation in Maude. WRLA Canh Minh Do, Kazuhiro Ogata
2024	J	`jnl`	Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer Protocol. IEEE Access Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani
2024	C	`ed.`	Formal Methods and Software Engineering - 25th International Conference on Formal Engineering Methods, ICFEM 2024, Hiroshima, Japan, December 2-6, 2024, Proceedings ICFEM Kazuhiro Ogata, Dominique Méry, Meng Sun, Shaoying Liu
2024	—	`conf`	Formal Specification and Model Checking of a Synchronous Leader Election Protocol in Maude. SFPVV Tomoyoshi Ogura, Canh Minh Do, Kazuhiro Ogata
2024	J	`jnl`	Integration of state machine graphical animation and Maude to facilitate characteristic conjecture: an approach to lemma discovery in theorem proving. Multim. Tools Appl. Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata, Adrián Riesco
2024	—	`ed.`	Rewriting Logic and Its Applications - 15th International Workshop, WRLA 2024, Luxembourg City, Luxembourg, April 6-7, 2024, Revised Selected Papers WRLA Kazuhiro Ogata, Narciso Martí-Oliet
2024	J	`jnl`	Symbolic model checking quantum circuits in Maude. PeerJ Comput. Sci. Canh Minh Do, Kazuhiro Ogata
2024	—	`conf`	Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ. WRLA Duong Dinh Tran, Kazuhiro Ogata
2023	J	`jnl`	A Layered and Parallelized Method of Eventual Model Checking. Inf. Yati Phyo, Moe Nandi Aung, Canh Minh Do, Kazuhiro Ogata
2023	—	`conf`	A way to find counterexamples located at deep positions with domain knowledge of authentication protocols. ICSCA Naomi Okumura, Kazuhiro Ogata
2023	—	`conf`	Automated Quantum Program Verification in Dynamic Quantum Logic. DaLí Tsubasa Takagi, Canh Minh Do, Kazuhiro Ogata
2023	—	`conf`	Formal Specification and Model Checking of Raft Leader Election in Maude. ICSCA Takanori Ishibashi, Kazuhiro Ogata
2023	—	`conf`	Formal Specification and Model Checking of Raft Log Replication in Maude. DMSVIVA Takanori Ishibashi, Kazuhiro Ogata
2023	J	`jnl`	Graphical Animations of an Autonomous Vehicle Merging Protocol. J. Vis. Lang. Comput. Dang Duy Bui, Minxuan Liu, Duong Ding Tran, Kazuhiro Ogata
2023	J	`jnl`	Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version. PeerJ Comput. Sci. Duong Dinh Tran, Canh Minh Do, Santiago Escobar, Kazuhiro Ogata
2023	J	`jnl`	Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude. IET Inf. Secur. Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani
2023	J	`jnl`	Modelling and verification of post-quantum key encapsulation mechanisms using Maude. PeerJ Comput. Sci. Víctor García, Santiago Escobar, Kazuhiro Ogata, Sedat Akleylek, Ayoub Otmani
2023	J	`jnl`	Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way. ACM Trans. Softw. Eng. Methodol. Canh Minh Do, Yati Phyo, Adrián Riesco, Kazuhiro Ogata
2023	J	`jnl`	Selected papers from the 15th international symposium on Theoretical Aspects of Software Engineering (TASE 2021). Sci. Comput. Program. Min Zhang, Kazuhiro Ogata
2023	C	`conf`	Symbolic Model Checking Quantum Circuits in Maude. SEKE Canh Minh Do, Kazuhiro Ogata
2023	J	`jnl`	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. Duong Dinh Tran, Thet Wai Mon, Kazuhiro Ogata
2022	J	`jnl`	A Divide & Conquer Approach to Leads-to Model Checking. Comput. J. Yati Phyo, Canh Minh Do, Kazuhiro Ogata
2022	—	`conf`	A Tool for Model Checking Eventual Model Checking in a Stratified Way. DSA Moe Nandi Aung, Yati Phyo, Canh Minh Do, Kazuhiro Ogata
2022	C	`conf`	A divide and conquer approach to until and until stable model checking. SEKE Canh Minh Do, Yati Phyo, Kazuhiro Ogata
2022	J	`jnl`	An integrated tool set for verifying CafeOBJ specifications. J. Syst. Softw. Adrián Riesco, Kazuhiro Ogata
2022	J	`jnl`	Better state pictures facilitating state machine characteristic conjecture. Multim. Tools Appl. Dang Duy Bui, Kazuhiro Ogata
2022	C	`conf`	Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude. SEKE Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani
2022	—	`conf`	Formal specification and model checking of lattice-based key encapsulation mechanisms in Maude. FAVPQC@ICFEM Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani
2022	J	`jnl`	Formal verification of TLS 1.2 by automatically generating proof scores. Comput. Secur. Duong Dinh Tran, Kazuhiro Ogata
2022	—	`conf`	Graphical Animations of an Autonomous Vehicle Merging Protocol. DMSVIVA Minxuan Liu, Kazuhiro Ogata, Dang Duy Bui
2022	J	`jnl`	Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol. J. Vis. Lang. Comput. Dang Duy Bui, Win Hlaing Hlaing Myint, Duong Dinh Tran, Kazuhiro Ogata
2022	—	`conf`	Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security analysis. FAVPQC@ICFEM Duong Dinh Tran, Canh Minh Do, Santiago Escobar, Kazuhiro Ogata
2022	B	`conf`	IPSG: Invariant Proof Score Generator. COMPSAC Duong Dinh Tran, Kazuhiro Ogata
2022	—	`conf`	Integration of SMGA and Maude to Facilitate Characteristic Conjecture. DMSVIVA Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata, Adrián Riesco
2022	—	`conf`	Modeling and verification of the post-quantum key encapsulation mechanism KYBER using Maude. FAVPQC@ICFEM Víctor García, Santiago Escobar, Kazuhiro Ogata
2022	—	`conf`	Parallel Maude-NPA for Cryptographic Protocol Analysis. WRLA Canh Minh Do, Adrián Riesco, Santiago Escobar, Kazuhiro Ogata
2022	J	`jnl`	Parallel Specification-Based Testing for Concurrent Programs. IEEE Access Canh Minh Do, Kazuhiro Ogata
2022	—	`ed.`	Proceedings of the International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols co-located with the 23rd International Conference on Formal Engineering Methods (ICFEM 2022), Madrid, Spain, October 24, 2022. FAVPQC@ICFEM Sedat Akleylek, Santiago Escobar, Kazuhiro Ogata, Ayoub Otmani
2022	J	`jnl`	Sequential and Parallel Tools for Model Checking Conditional Stable Properties in a Layered Way. IEEE Access Canh Minh Do, Yati Phyo, Kazuhiro Ogata
2022	J	`jnl`	Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. Masaki Nakamura, Shuki Higashi, Kazutoshi Sakakibara, Kazuhiro Ogata
2022	J	`jnl`	Specifying and Model Checking Distributed Control Algorithms at Meta-level. Comput. J. Ha Thi Thu Doan, Kazuhiro Ogata
2021	C	`conf`	A Divide & Conquer Approach to Conditional Stable Model Checking. ICTAC Yati Phyo, Canh Minh Do, Kazuhiro Ogata
2021	B	`conf`	A support tool for the L + 1-layer divide & conquer approach to leads-to model checking. COMPSAC Yati Phyo, Canh Minh Do, Kazuhiro Ogata
2021	—	`conf`	Formal Specification and Model Checking of an Autonomous Vehicle Merging Protocol. QRS Companion Minxuan Liu, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata
2021	J	`jnl`	Formal Verification of Multitask Hybrid Systems by the OTS/CafeOBJ Method. Int. J. Softw. Eng. Knowl. Eng. Masaki Nakamura, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata
2021	C	`conf`	Formal specification and model checking of a recoverable wait-free version of MCS. SEKE Duong Dinh Tran, Kentaro Waki, Kazuhiro Ogata
2021	C	`conf`	Formal verification of Anderson mutual exclusion protocol by introducing an auxiliary variable (S). SEKE Naoki Asae, Duong Dinh Tran, Kazuhiro Ogata
2021	C	`conf`	Formal verification of IFF and NSLPK authentication protocols with CiMPG (S). SEKE Thet Wai Mon, Shuho Fujii, Duong Dinh Tran, Kazuhiro Ogata
2021	C	`conf`	Formal verification of multitask hybrid systems by the OTS/CafeOBJ method. SEKE Masaki Nakamura, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata
2021	—	`conf`	Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S). DMSVIVA Win Hlaing Hlaing Myint, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata
2021	J	`jnl`	Graphical Animations of the NS(L)PK Authentication Protocols. J. Vis. Lang. Comput. Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, Canh Minh Do, Kazuhiro Ogata
2021	—	`conf`	Graphical Animations of the NSLPK Authentication Protocol (S). DMSVIVA Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata
2021	J	`jnl`	Simulation-Based Invariant Verification Technique for the OTS/CafeOBJ Method. IEEE Access Duong Dinh Tran, Dang Duy Bui, Kazuhiro Ogata
2020	J	`jnl`	A Generic Approach on How to Formally Specify and Model Check Path Finding Algorithms: Dijkstra, A* and LPA. Int. J. Softw. Eng. Knowl. Eng. Kazuhiro Ogata
2020	C	`conf`	A divide & conquer approach to testing concurrent programs with JPF APSEC Canh Minh Do, Kazuhiro Ogata
2020	—	`conf`	Better State Pictures Facilitating State Machine Characteristic Conjecture. DMSVIVA Dang Duy Bui, Kazuhiro Ogata
2020	C	`conf`	CiMPG+F: A Proof Generator and Fixer-Upper for CafeOBJ Specifications. ICTAC Adrián Riesco, Kazuhiro Ogata
2020	J	`jnl`	Formal analysis of RFC 8120 authentication protocol for HTTP under different assumptions. J. Inf. Secur. Appl. Naomi Okumura, Kazuhiro Ogata, Yoichi Shinoda
2020	—	`conf`	Formal verification of Fischer's real-time mutual exclusion protocol by the OTS/CafeOBJ method. SICE Masaki Nakamura, Shuki Higashi, Kazutoshi Sakakibara, Kazuhiro Ogata
2020	C	`conf`	Formal verification of an abstract version of Anderson protocol with CafeOBJ, CiMPA and CiMPG. SEKE Duong Dinh Tran, Kazuhiro Ogata
2020	C	`conf`	Lemma Weakening for State Machine Invariant Proofs. APSEC Duong Dinh Tran, Dang Duy Bui, Parth Gupta, Kazuhiro Ogata
2020	—	`conf`	Parallel stratified random testing for concurrent programs. QRS Companion Canh Minh Do, Kazuhiro Ogata
2020	J	`jnl`	Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method. CoRR Masaki Nakamura, Kazutoshi Sakakibara, Kazuhiro Ogata
2020	J	`jnl`	Stability of termination and sufficient-completeness under pushouts via amalgamation. Theor. Comput. Sci. Daniel Gaina, Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
2019	—	`conf`	A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and Maude. SOFL+MSVL Canh Minh Do, Kazuhiro Ogata
2019	J	`jnl`	A More Faithful Formal Definition of the Desired Property for Distributed Snapshot Algorithms to Model Check the Property. Comput. Informatics Ha Thi Thu Doan, Kazuhiro Ogata
2019	J	`jnl`	A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions. Frontiers Comput. Sci. Kazuhiro Ogata
2019	C	`conf`	An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms. SSS Ha Thi Thu Doan, Adrián Riesco, Kazuhiro Ogata
2019	C	`conf`	Formal Specification and Model Checking of A* Algorithm. SEKE Kazuhiro Ogata
2019	—	`conf`	Formal Specification and Model Checking of a Ride-sharing System in Maude. SOFL+MSVL Eiichi Muramoto, Kazuhiro Ogata, Yoichi Shinoda
2019	C	`conf`	Formal Specification and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S). SEKE Moe Nandi Aung, Yati Phyo, Kazuhiro Ogata
2019	—	`conf`	Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol. DMSVIVA Dang Duy Bui, Kazuhiro Ogata
2019	J	`jnl`	Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol. J. Vis. Lang. Comput. Dang Duy Bui, Kazuhiro Ogata
2019	B	`conf`	KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs. FASE Jiaqi Qian, Min Zhang, Yi Wang, Kazuhiro Ogata
2019	C	`conf`	Specification-based Testing with Simulation Relations (S). SEKE Canh Minh Do, Kazuhiro Ogata
2018	—	`conf`	Analysis of Some Variants of the Anderson Array-Based Queuing Mutual Exclusion Protocol with Model Checking and Graphical Animations. DSA Yati Phyo, Kazuhiro Ogata
2018	—	`conf`	Analysis of Two Flawed Versions of A Mutual Exclusion Protocol with Maude and SMGA. ICSCA May Thu Aung, Tam Thi Thanh Nguyen, Kazuhiro Ogata
2018	C	`conf`	Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks. APSEC Yati Phyo, Kazuhiro Ogata
2018	J	`jnl`	Formal analysis of a security protocol for e-passports based on rewrite theory specifications. J. Inf. Secur. Appl. Manjukeshwar Reddy Mandadi, Varuneshwar Reddy Mandadi, Kazuhiro Ogata
2018	J	`jnl`	From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories. Theor. Comput. Sci. Min Zhang, Kazuhiro Ogata
2018	—	`conf`	Guessing Properties of the Qlock Mutual Exclusion Protocol based on its Graphical Animations and confirming the Properties by Model Checking. ICSCA May Thu Aung, Tam Thi Thanh Nguyen, Kazuhiro Ogata
2018	—	`conf`	Model Checking of the Suzuki-Kasami Distributed Mutual Exclusion Algorithm with SPIN. DSA Shouki Sakamoto, Kazuhiro Ogata
2018	J	`jnl`	Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores. ACM Trans. Softw. Eng. Methodol. Adrián Riesco, Kazuhiro Ogata
2017	C	`conf`	A Formal Proof Generator from Semi-formal Proof Documents. ICTAC Adrián Riesco, Kazuhiro Ogata
2017	J	`jnl`	A Maude environment for CafeOBJ. Formal Aspects Comput. Adrián Riesco, Kazuhiro Ogata, Kokichi Futatsugi
2017	—	`conf`	A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler. SOFL+MSVL Dorian Daudier, Trinh Ngoc Quoc Bao, Kazuhiro Ogata
2017	—	`conf`	A Way to Comprehend Counterexamples Generated by the Maude LTL Model Checker. SATE Tam Thi Thanh Nguyen, Kazuhiro Ogata
2017	—	`conf`	Graphical Animations of State Machines. DASC/PiCom/DataCom/CyberSciTech Tam Thi Thanh Nguyen, Kazuhiro Ogata
2017	—	`conf`	Graphically Perceiving Characteristics of the MCS Lock and Model Checking Them. SOFL+MSVL Tam Thi Thanh Nguyen, Kazuhiro Ogata
2017	B	`conf`	Model Checking of Robot Gathering. OPODIS Ha Thi Thu Doan, François Bonnet, Kazuhiro Ogata
2017	J	`jnl`	Model checking the iKP electronic payment protocols. J. Inf. Secur. Appl. Kazuhiro Ogata
2017	A	`conf`	Specifying a Distributed Snapshot Algorithm as a Meta-Program and Model Checking it at Meta-Level. ICDCS Ha Thi Thu Doan, Kazuhiro Ogata, François Bonnet
2017	C	`conf`	Writing Concurrent Java Programs Based on CafeOBJ Specifications. APSEC Xuan-Linh Ha, Kazuhiro Ogata
2016	B	`conf`	CafeInMaude: A CafeOBJ Interpreter in Maude. FASE Adrián Riesco, Kazuhiro Ogata, Kokichi Futatsugi
2016	C	`ed.`	Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings ICFEM Kazuhiro Ogata, Mark Lawford, Shaoying Liu
2016	J	`jnl`	Formal modeling and analysis of time- and resource-sensitive simple business processes. J. Inf. Secur. Appl. Kazuhiro Ogata, Thapana Chaimanont, Min Zhang
2016	—	`conf`	Model Checking of a Mobile Robots Perpetual Exploration Algorithm. SOFL+MSVL Ha Thi Thu Doan, François Bonnet, Kazuhiro Ogata
2015	—	`conf`	Case Studies on Extracting the Characteristics of the Reachable States of State Machines Formalizing Communication Protocols with Inductive Logic Programing. ILP (Late Breaking Papers) Dung Tuan Ho, Min Zhang, Kazuhiro Ogata
2015	C	`conf`	Formalization and Verification of Declarative Cloud Orchestration. ICFEM Hiroyuki Yoshida, Kazuhiro Ogata, Kokichi Futatsugi
2015	—	`conf`	Proving Sufficient Completeness of Constructor-Based Algebraic Specifications. CSA/CUTE Masaki Nakamura, Daniel Gâinâ, Kazuhiro Ogata, Kokichi Futatsugi
2015	C	`conf`	Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates. APSEC Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
2014	—	`conf`	A Formal Semantics of the OSEK/VDX Standard in $${\mathbb {K}}$$ Framework and Its Applications. WRLA Min Zhang, Yunja Choi, Kazuhiro Ogata
2014	—	`conf`	Evaluation of Maude as a Test Generation Engine for Automotive Operating Systems. APSEC (1) Yunja Choi, Min Zhang, Kazuhiro Ogata
2014	—	`conf`	Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications. Specification, Algebra, and Software Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
2014	C	`conf`	Liveness Properties in CafeOBJ - A Case Study for Meta-Level Specifications. LOPSTR Norbert Preining, Kazuhiro Ogata, Kokichi Futatsugi
2014	—	`conf`	On Automation of OTS/CafeOBJ Method. Specification, Algebra, and Software Daniel Gâinâ, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi
2014	—	`ed.`	Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi Specification, Algebra, and Software Shusaku Iida, José Meseguer, Kazuhiro Ogata
2014	J	`jnl`	TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned. IEICE Trans. Inf. Syst. Iakovos Ouranos, Kazuhiro Ogata, Petros S. Stefaneas
2014	—	`conf`	Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs. Specification, Algebra, and Software Kazuhiro Ogata, Kokichi Futatsugi
2014	—	`conf`	Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method. Specification, Algebra, and Software Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
2013	B	`conf`	A Divide and Conquer Approach to Model Checking of Liveness Properties. COMPSAC Kazuhiro Ogata, Min Zhang
2013	J	`jnl`	Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method. J. Univers. Comput. Sci. Kazuhiro Ogata, Kokichi Futatsugi
2013	J	`jnl`	Foreword. IEICE Trans. Inf. Syst. Kazuhiro Ogata
2013	—	`conf`	Formalization and Verification of Behavioral Correctness of Dynamic Software Updates. VSSE Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
2013	—	`conf`	Model Checking Liveness Properties under Fairness & Anti-fairness Assumptions. APSEC (1) Kazuhiro Ogata
2012	C	`conf`	An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms. APSEC Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
2012	J	`jnl`	Constructor-based Logics. J. Univers. Comput. Sci. Daniel Gâinâ, Kokichi Futatsugi, Kazuhiro Ogata
2012	—	`conf`	Formal Analysis of TESLA Protocol in the Timed OTS/CafeOBJ Method. ISoLA (2) Iakovos Ouranos, Kazuhiro Ogata, Petros S. Stefaneas
2012	C	`conf`	Invariant-preserved Transformation of State Machines from Equations into Rewrite Rules. APSEC Min Zhang, Kazuhiro Ogata
2012	J	`jnl`	Principles of proof scores in CafeOBJ. Theor. Comput. Sci. Kokichi Futatsugi, Daniel Gâinâ, Kazuhiro Ogata
2012	C	`conf`	Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic. ICFEM Kazuhiro Ogata, Thi Thanh Huyen Phan
2011	J	`jnl`	Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support. IEICE Trans. Inf. Syst. Min Zhang, Kazuhiro Ogata, Masaki Nakamura
2010	C	`conf`	A Combination of Forward and Backward Reachability Analysis Methods. ICFEM Kazuhiro Ogata, Kokichi Futatsugi
2010	—	`conf`	Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method. ISoLA (1) Iakovos Ouranos, Petros S. Stefaneas, Kazuhiro Ogata
2010	J	`jnl`	Proof Score Approach to Analysis of Electronic Commerce Protocols. Int. J. Softw. Eng. Knowl. Eng. Kazuhiro Ogata, Kokichi Futatsugi
2010	J	`jnl`	Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications. J. Symb. Comput. Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
2010	C	`conf`	Specification Translation of State Machines from Equational Theories into Rewrite Theories. ICFEM Min Zhang, Kazuhiro Ogata, Masaki Nakamura
2010	J	`jnl`	Towards Reliable E-Government Systems with the OTS/CafeOBJ Method. IEICE Trans. Inf. Syst. Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
2009	B	`conf`	Constructor-Based Institutions. CALCO Daniel Gâinâ, Kokichi Futatsugi, Kazuhiro Ogata
2009	—	`conf`	Modular Implementation of a Translator from Behavioral Specifications to Rewrite Theory Specifications. QSIC Min Zhang, Kazuhiro Ogata
2009	J	`jnl`	User-Defined On-Demand Matching. IEICE Trans. Inf. Syst. Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
2008	J	`jnl`	A Specification Translation from Behavioral Specifications to Rewrite Specifications. IEICE Trans. Inf. Syst. Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
2008	C	`conf`	Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes. ICFEM Kazuhiro Ogata, Kokichi Futatsugi
2008	J	`jnl`	Proof Score Approach to Verification of Liveness Properties. IEICE Trans. Inf. Syst. Kazuhiro Ogata, Kokichi Futatsugi
2008	C	`conf`	Trace anonymity in the OTS/CafeOBJ method. CIT Weiqiang Kong, Kazuhiro Ogata, Jian Cheng, Kokichi Futatsugi
2007	B	`conf`	Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System. IFM Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
2007	J	`jnl`	Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. Kazuhiro Ogata, Kokichi Futatsugi
2007	J	`jnl`	CrÈme: an Automatic Invariant Prover of Behavioral Specifications. Int. J. Softw. Eng. Knowl. Eng. Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, Kokichi Futatsugi
2007	J	`jnl`	From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ. Inf. Media Technol. Jianwen Xiang, Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi
2007	J	`jnl`	Modeling and verification of real-time systems based on equations. Sci. Comput. Program. Kazuhiro Ogata, Kokichi Futatsugi
2007	—	`conf`	Simulation-based Verification for Invariant Properties in the OTS/CafeOBJ Method. REFINE@IFM Kazuhiro Ogata, Kokichi Futatsugi
2007	J	`jnl`	Specification and Verification of Workflows with Rbac Mechanism and Sod Constraints. Int. J. Softw. Eng. Knowl. Eng. Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
2007	J	`jnl`	State Machines as Inductive Types. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. Kazuhiro Ogata, Kokichi Futatsugi
2006	—	`conf`	Analysis of Positive Incentives for Protecting Secrets in Digital Rights Management. WEBIST (2) Jianwen Xiang, Weiqiang Kong, Kokichi Futatsugi, Kazuhiro Ogata
2006	—	`conf`	Automating Invariant Verification of Behavioral Specifications. QSIC Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, Kokichi Futatsugi
2006	C	`conf`	Falsification of OTSs by Searches of Bounded Reachable State Spaces. SEKE Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi
2006	C	`conf`	Induction-Guided Falsification. ICFEM Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi
2006	—	`conf`	Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method. Essays Dedicated to Joseph A. Goguen Kazuhiro Ogata, Kokichi Futatsugi
2005	C	`conf`	A Lightweight Integration of Theorem Proving and Model Checking for System Verification. APSEC Weiqiang Kong, Takahiro Seino, Kokichi Futatsugi, Kazuhiro Ogata
2005	—	`conf`	A Toolkit for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method. RULE@RDP Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
2005	C	`conf`	Analysis of the Suzuki-Kasami Algorithm with SAL Model Checkers. CIT Kazuhiro Ogata, Kokichi Futatsugi
2005	C	`conf`	Analysis of the Suzuki-Kasami Algorithm with the Maude Model Checker. APSEC Kazuhiro Ogata, Kokichi Futatsugi
2005	C	`conf`	Chocolat/SMV: A Translator from CafeOBJ into SMV. PDCAT Kazuhiro Ogata, Masahiro Nakano, Masaki Nakamura, Kokichi Futatsugi
2005	A	`conf`	Equational Approach to Formal Analysis of TLS. ICDCS Kazuhiro Ogata, Kokichi Futatsugi
2005	C	`conf`	Formal Analysis of Workflow Systems with Security Considerations. SEKE Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
2005	—	`conf`	Formal Fault Tree Analysis of State Transition Systems. QSIC Jianwen Xiang, Kazuhiro Ogata
2005	J	`jnl`	Mechanically supporting case analysis for verification of distributed systems. Int. J. Pervasive Comput. Commun. Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
2005	C	`conf`	Proof Score Approach to Verification of Liveness Properties. SEKE Kazuhiro Ogata, Kokichi Futatsugi
2005	C	`conf`	Provably Correct Translation from CafeOBJ into Java. SEKE Jittisak Senachak, Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
2005	—	`conf`	Verifying Design with Proof Scores. VSTTE Kokichi Futatsugi, Joseph A. Goguen, Kazuhiro Ogata
2004	—	`conf`	Equational Approach to Formal Verification of SET. QSIC Kazuhiro Ogata, Kokichi Futatsugi
2004	C	`conf`	Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol. CIT Weiqiang Kong, Kazuhiro Ogata, Jianwen Xiang, Kokichi Futatsugi
2004	—	`conf`	Modeling and Verification of Hybrid Systems Based on Equations. DIPES Kazuhiro Ogata, Daigo Yamagishi, Takahiro Seino, Kokichi Futatsugi
2004	C	`conf`	Supporting Case Analysis with Algebraic Specification Languages. CIT Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
2003	J	`jnl`	CafeOBJ: Logical Foundations and Methodologies. Comput. Artif. Intell. Razvan Diaconescu, Kokichi Futatsugi, Kazuhiro Ogata
2003	J	`jnl`	Flaw and modification of the iKP electronic payment protocols. Inf. Process. Lett. Kazuhiro Ogata, Kokichi Futatsugi
2003	—	`conf`	Formal Analysis of the NetBill Electronic Commerce Protocol. ISSS Kazuhiro Ogata, Kokichi Futatsugi
2003	B	`conf`	Formal Verification of the Horn-Preneel Micropayment Protocol. VMCAI Kazuhiro Ogata, Kokichi Futatsugi
2003	—	`conf`	Proof Scores in the OTS/CafeOBJ Method. FMOODS Kazuhiro Ogata, Kokichi Futatsugi
2002	—	`conf`	Formal Analysis of Suzuki & Kasami Distributed Mutual Exclusion Algorithm. FMOODS Kazuhiro Ogata, Kokichi Futatsugi
2002	—	`conf`	Formal Analysis of the ISSS Kazuhiro Ogata, Kokichi Futatsugi
2002	—	`conf`	Rewriting-Based Verification of Authentication Protocols. WRLA Kazuhiro Ogata, Kokichi Futatsugi
2001	—	`conf`	Formally Modeling and Verifying Ricart&Agrawala Distributed Mutual Exclusion Algorithm. APAQS Kazuhiro Ogata, Kokichi Futatsugi
2001	A*	`conf`	Modeling and Verification of Distributed Real-Time Systems Based on CafeOBJ. ASE Kazuhiro Ogata, Kokichi Futatsugi
2001	A	`conf`	Specifying and verifying a railroad crossing with CafeOBJ. IPDPS Kazuhiro Ogata, Kokichi Futatsugi
2000	—	`conf`	Operational Semantics of Rewriting with the On-demand Evaluation Strategy. SAC (2) Kazuhiro Ogata, Kokichi Futatsugi
2000	—	`conf`	The evaluation strategy for head normal form with and without on-demand flags. WRLA Masaki Nakamura, Kazuhiro Ogata
1999	—	`conf`	Formal Verification of the MCS List-Based Queuing Lock. ASIAN Kazuhiro Ogata, Kokichi Futatsugi
1999	Misc	`conf`	Optimizing Term Rewriting Using Discrimination Nets With Specialization. SAC Kazuhiro Ogata, Shigenori Ioroi, Kokichi Futatsugi
1998	—	`conf`	Experimental Implementation of Parallel TRAM on Massively Parallel Computer. Euro-Par Kazuhiro Ogata, Hiromichi Hirata, Shigenori Ioroi, Kokichi Futatsugi
1997	—	`conf`	Design and Implementation of Parallel TRAM. Euro-Par Kazuhiro Ogata, Masaru Kondo, Shigenori Ioroi, Kokichi Futatsugi
1997	—	`conf`	Implementation of Term Rewritings with the Evaluation Strategy. PLILP Kazuhiro Ogata, Kokichi Futatsugi
1997	—	`conf`	TRAM: An Abstract Machine for Order-Sorted Conditioned Term Rewriting Systems. RTA Kazuhiro Ogata, Koichi Ohhara, Kokichi Futatsugi
1994	Misc	`conf`	Object allocation and dynamic compilation in MultithreadSmalltalk. SAC Kazuhiro Ogata, Norihisa Doi
1992	—	`conf`	HoME: Smalltalk on the Match Environment. TOOLS (6) Kazuhiro Ogata, Satoshi Kurihara, Mikio Inari, Norihisa Doi
1992	A*	`conf`	The Design and Implementation of HoME. PLDI Kazuhiro Ogata, Satoshi Kurihara, Mikio Inari, Norihisa Doi