Parallel Maude-NPA for Cryptographic Protocol Analysis Canh Minh Do, Adrián Riesco, Santiago Escobar, Kazuhiro Ogata
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 13252 LNCS, 253-273, 2022
Better State Pictures Facilitating State Machine Characteristic Conjecture
Dang Duy Bui, Kazuhiro Ogata
26th International DMS Conference on Visualization and Visual Languages, -, 2020
Formal verification of an abstract version of Anderson protocolwith CafeOBJ, CiMPA and CiMPG
Duong Dinh Tran, Kazuhiro Ogata
32nd International Conference on Software Engineering & Knowledge Engineering, -, 2020
Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol
Dang Duy Bui, Kazuhiro Ogata
Journal of Visual Language and Computing, -, 2019
Model Checking of Robot Gathering
Ha Thi Thu Doan, Francois Bonnet, Kazuhiro Ogata
21st International Conference on Principles of Distributed Systems (21st OPODIS), -, 2017
Graphical Animations of State Machines
Tam Thi Thanh Nguyen, Kazuhiro Ogata
15th IEEE International Conference on Dependable, Autonomic and Secure Computing (15th DASC), TBA-, 2017
Proving Sufficient Completeness of Constructor-Based Algebraic Specifications
Masaki Nakamura, Daniel Gaina, Kazuhiro Ogata, Kokichi Futatsugi
Advances in Computer Science and Ubiquitous Computing, LNEE 373 (Springer), 15-21-, 2015
Formalization and Verification of Declarative Cloud Orchestration
Hiroyuki Yoshida, Kazuhiro Ogata, Kokichi Futatsugi
Formal Methods and Software Engineering - 17th International Conferenceon Formal Engineering Methods, (ICFEM 2015),Lecture Notes in Computer Science, Springer, 9407, 33-49-, 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, Kazuhiro Ogata
ILP (Late Breaking Papers) 2015, 33-47, 2015
On Automation of OTS/CafeOBJ Method
Daniel Gaina, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi
Lecture Notes in Computer Science, 8373, 578, 25-, 2014
Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
Specification, Algebra, and Software 2014, 92-109-, 2014
Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
Specification, Algebra, and Software 2014, 560-577-, 2014
Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
Kazuhiro Ogata, Kokichi Futatsugi
Specification, Algebra, and Software 2014, 630-656-, 2014
Formalization and Verification of Behavioral Correctness of Dynamic Software Updates
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
Electr. Notes Theor. Comput. Sci., 294, 12-23-, 2013
Formal Analysis of TESLA Protocol in the Timed OTS/CafeOBJ Method
Iakovos Ouranos, Kazuhiro Ogata, Petros Stefaneas
ISoLA 2012, Part II, LNCS 7610, Springer, pp.126-142-, 2012
Specification and Model Checking of the Chandy and Lamport Distributed Snapshot Algorithm in Rewriting Logic
Kazuhiro Ogata, Phan Thi Thanh Huyen
ICFEM 2012, LNCS 7635, Springer, 87-102-, 2012
Constructor-based Logics Daniel Gaina, Kokichi Futatsugi, Kazuhiro Ogata
JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 18, 16, 2204-2233, 2012
Constructor-Based Institutions Daniel Gaina, Kokichi Futatsugi, Kazuhiro Ogata
ALGEBRA AND COALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, 5728, 398-412, 2009
Analysis of Membership Sharing Problem in Digital Subscription Services
Jianwen Xiang, Jing Tian, Kazuhiro Ogata, Akira Mori, Kokichi Futatsugi
International Journal of Revenue Management, Inderscience Publishers, -, 2009
Introducing CafeOBJ (4) : Verification with Proof Scores FUTATSUGI Kokichi, OGATA Kazuhiro, NAKAMURA Masaki, Kokichi Futatsugi, Kazuhiro Ogata, Masaki Nakamura, Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST), Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST), School of Electrical and Computer Engineering Kanazawa University
コンピュータソフトウェア, 25, 4, 68-84, 2008
Introducing CafeOBJ(3) : Equational Reasoning and Term Rewriting Systems NAKAMURA Masaki, FUTATSUGI Kokichi, OGATA Kazuhiro, Masaki Nakamura, Kokichi Futatsugi, Kazuhiro Ogata, School of Electrical and Computer Engineering Kanazawa University, Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST), Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST)
Computer Software, 25, 3, 69-80, 2008
Introducing CafeOBJ (1) : Formal Methods and CafeOBJ FUTATSUGI Kokichi, OGATA Kazuhiro, NAKAMURA Masaki, Kokichi Futatsugi, Kazuhiro Ogata, Masaki Nakamura, Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST), Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST), Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST)
コンピュータソフトウェア, 25, 2, 1-13, 2008
Introducing CafeOBJ (2) : Syntax and Semantics NAKAMURA Masaki, FUTATSUGI Kokichi, OGATA Kazuhiro, Masaki Nakamura, Kokichi Futatsugi, Kazuhiro Ogata, Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST), Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST), Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST)
Computer Software, 25, 2, 14-27, 2008
Trace anonymity in the OTS/CafeOBJ method Weiqiang Kong, Kazuhiro Ogata, Jian Cheng, Kokichi Futatsugi
2008 IEEE 8TH INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION TECHNOLOGY, VOLS 1 AND 2, 754-759, 2008
Simulation-based verification for invariant properties in the OTS/CafeOBJ method
Kazuhiro Ogata, Kokichi Futatsugi
Proceedings of the 4th International Refinement Workshop (Refine 2007), ENTCS 201, Elsevier, 127-154-, 2008
State machines as inductive types Kazuhiro Ogata, Kokichi Futatsugi
IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, E90A, 12, 2985-2988, 2007
Induction-guided falsification Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi
FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 4260, 114-131, 2006
Model-Checking Observational Transition System with Maude
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
20th International Technical Conference on Circuits/Systems, Computers and Communications (20th ITC-CSCC), 5-6, 2005
Mechanically Supporting Case Analysis for Verification of Distributed Systems
Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
Journal of Pervasive Computing and Communications, Troubador, 1, 2, 135-145-, 2005
書き換えによるOtway-Rees認証プロトコルの検証
清野貴博, 加藤淳, 緒方和博
第11回ソフトウェア工学の基礎ワークショップ(第11回FOSE), 153-156, 2004
SMVによるOTS/CafeOBJ仕様のモデル検査
中野昌弘, 中村正樹, 緒方和博, 二木厚吉
第11回ソフトウェア工学の基礎ワークショップ(第11回FOSE), 129-140, 2004
Inductive Verification of Security Protocols with Rewriting OGATA Kazuhiro, FUTATSUGI Kokichi, Kazuhiro Ogata, Kokichi Futatsugi, NEC Software Hokuriku Ltd. : Japan Advanced Institute of Science and Technology(JAIST), Japan Advanced Institute of Science and Technology(JAIST)
Computer Software, 20, 3, 54-72, 2003
Automatic Verification of the STS Authentication Protocol with Creme
Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, Kokichi Futatsugi
20th International Technical Conference on Circuits/Systems, Computers and Communications (20th ITC-CSCC), 15-16, 2003
Provably Correct Translation from CafeOBJ into Java
Jittisak Senachak, Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
17th International Conference on Software Engineering and Knowledge Engineering (17th SEKE), 614-619, 2003
項書換えを用いた安全性検証の組織化
清野貴博, 緒方和博, 二木厚吉
第9回ソフトウェア工学の基礎ワークショップ(第9回FOSE), 107-118, 2002
実時間制約を考慮したマルチタスキングのモデル化
清野貴博, 緒方和博, 二木厚吉, 日比野靖
第8回ソフトウェア工学の基礎ワークショップ(第8回FOSE), 143-146, 2001
Specification and verification of a single-track railroad signaling in CafeOBJ
Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
2000 International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2000), 268-273, 2000
代数仕様言語CafeOBJによる鉄道信号システムの記述と検証
清野貴博, 緒方和博, 二木厚吉
第6回ソフトウェア工学の基礎ワークショップ(第6回FOSE), 180-187, 1999
Specification and verification of some classical mutual exclusion algorithms with CafeOBJ
Kazuhiro Ogata, Kokichi Futatsugi
OBJ/CafeOBJ/Maude Workshop at Formal Methods 1999, 159-177, 1999
CafeOBJのモジュールシステムの設計およびCafeOBJによる検証
五百蔵重典, 緒方和博, 二木厚吉
第5回ソフトウェア工学の基礎ワークショップ(第5回FOSE), 209-218, 1998
How to give local strategies to function symbols for equality of two implementations of the E-strategy with and without evaluated flags
Takashi Nagaya, Michihiro Matsumoto, Kazuhiro Ogata, Kokichi Futatsugi
3rd Asian Symposium on Computer Mathematics (3rd ASCM),, -, 1998
項の構造を考慮したAC照合
五百蔵重典, 緒方和博, 二木厚吉
第3回ソフトウェア工学の基礎ワークショップ(第3回FOSE), 106-109, 1996
MultithreadSmalltalk. Ogata Kazuhiro, Kurihara Satoshi, Inari Mikio, Doi Norihisa
Computer Software, 11, 4, 4_325-4_342, 1994
HoME: Smalltalk on Mach environment
Kazuhiro Ogata, Satoshi Kurihara, Mikio Inari, Norihisa Doi
6th International Conference on Technology of Object-Oriented Languages and Systems (6th TOOLS),, -, 1991