TOP  >  Personal Info.  >  Published Papers
OGATA, Kazuhiro Professor, Director of Research Center for Integrated Science
Information Science, Computing Science, Research Center for Advanced Computing Infrastructure

Published Papers

181 items
Formal analysis of RFC 8120 authentication protocol for HTTP under different assumptions
Naomi Okumura, Kazuhiro Ogata, Yoichi Shinoda
JOURNAL OF INFORMATION SECURITY AND APPLICATIONS, 53, 102529-102529, 2020
A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions
Kazuhiro Ogata
FRONTIERS OF COMPUTER SCIENCE, 13, 1, 51-72, 2019
Formal analysis of a security protocol for e-passports based on rewrite theory specifications
Manjukeshwar Reddy Mandadi, Varuneshwar Reddy Mandadi, Kazuhiro Ogata
JOURNAL OF INFORMATION SECURITY AND APPLICATIONS, 42, 71-86, 2018
Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores
Adrian Riesco, Kazuhiro Ogata
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 27, 2, 6-32, 2018
From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories
Min Zhang, Kazuhiro Ogata
THEORETICAL COMPUTER SCIENCE, 722, 52-75, 2018
A Maude environment for CafeOBJ
Adrian Riesco, Kazuhiro Ogata, Kokichi Futatsugi
FORMAL ASPECTS OF COMPUTING, 29, 2, 309-334, 2017
Specifying a Distributed Snapshot Algorithm as a Meta-program and Model Checking it at Meta-level
Ha Thi Thu Doan, Kazuhiro Ogata, Francois Bonnet
2017 IEEE 37TH INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS (ICDCS 2017), 1586-1596, 2017
Principles of proof scores in CafeOBJ
Kokichi Futatsugi, Daniel Gaina, Kazuhiro Ogata
THEORETICAL COMPUTER SCIENCE, 464, 90-112, 2012
PROOF SCORE APPROACH TO ANALYSIS OF ELECTRONIC COMMERCE PROTOCOLS
Kazuhiro Ogata, Kokichi Futatsugi
INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 20, 2, 253-287, 2010
Creme: An automatic invariant prover of behavioral specifications
Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, Kokichi Futatsugi
INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 17, 6, 783-804, 2007
Modeling and verification of real-time systems based on equations
Kazuhiro Ogata, Kokichi Futatsugi
SCIENCE OF COMPUTER PROGRAMMING, 66, 2, 162-180, 2007
Some tips on writing proof scores in the OTS/CafeOBJ method
Kazuhiro Ogata, Kokichi Futatsugi
ALGEBRA, MEANING, AND COMPUTATION, 4060, 596-615, 2006
Equational approach to formal analysis of TLS
K Ogata, K Futatsugi
25th IEEE International Conference on Distributed Computing Systems, Proceedings, 795-804, 2005
Flaw and modification of the iKP electronic payment protocols
K Ogata, K Futatsugi
INFORMATION PROCESSING LETTERS, 86, 2, 57-62, 2003
Proof Scores in the OTS/CafeOBJ Method
Kazuhiro Ogata, Kokichi Futatsugi
Lecture Notes in Computer Science, 170-184, 2003
Modeling and verification of distributed real-time systems based on CafeOBJ
K. Ogata, K. Futatsugi
Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), -, 2001
The Design and Implementation of HoME
Kazuhiro Ogata, Satoshi Kurihara, Mikio Inari, Norihisa Doi
ACM SIGPLAN Notices, 27, 7, 44-54, 1992
Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way
Canh Minh Do, Yati Phyo, Adrián Riesco, Kazuhiro Ogata
ACM Transactions on Software Engineering and Methodology, -, 2023
Symbolic Model Checking Quantum Circuits in Maude.
Canh Minh Do, Kazuhiro Ogata 0001
SEKE, 103-108, 2023
Automated Quantum Program Verification in Dynamic Quantum Logic.
Tsubasa Takagi, Canh Minh Do, Kazuhiro Ogata 0001
DaLí, 68-84, 2023
Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version.
Duong Dinh Tran, Canh Minh Do, Santiago Escobar 0001, Kazuhiro Ogata 0001
PeerJ Computer Science, 9, -1556, 2023
A Layered and Parallelized Method of Eventual Model Checking.
Yati Phyo, Moe Nandi Aung, Canh Minh Do, Kazuhiro Ogata 0001
Information(Inf.), 14, 7, 384-384, 2023
A Divide & Conquer Approach to Leads-to Model Checking
Yati Phyo, Canh Minh Do, Kazuhiro Ogata
Computer Journal, 65, 6, 1353-1364, 2022
Parallel Specification-Based Testing for Concurrent Programs
Canh Minh Do, Kazuhiro Ogata
IEEE Access, 10, 24955-24975, 2022
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
A divide & conquer approach to until and until stable model checking
Canh Minh Do, Yati Phyo, Kazuhiro Ogata
Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE, 388-393, 2022
A Tool for Model Checking Eventual Model Checking in a Stratified Way
Moe Nandi Aung, Yati Phyo, Canh Minh Do, Kazuhiro Ogata
Proceedings - 2022 9th International Conference on Dependable Systems and Their Applications, DSA 2022, 270-279, 2022
Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security analysis
Duong Dinh Tran, Canh Minh Do, Santiago Escobar, Kazuhiro Ogata
CEUR Workshop Proceedings, 3280, 50-64, 2022
Sequential and Parallel Tools for Model Checking Conditional Stable Properties in a Layered Way
Canh Minh Do, Yati Phyo, Kazuhiro Ogata
IEEE Access, 10, 133749-133765, 2022
Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method.
Masaki Nakamura 0001, Shuki Higashi, Kazutoshi Sakakibara, Kazuhiro Ogata 0001
IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, 105-A, 5, 823-832, 2022
A support tool for the L + 1-layer divide & conquer approach to leads-to model checking
Yati Phyo, Canh Minh Do, Kazuhiro Ogata
Proceedings - 2021 IEEE 45th Annual Computers, Software, and Applications Conference, COMPSAC 2021, 854-863, 2021
A divide and conquer approach to eventual model checking
Moe Nandi Aung, Yati Phyo, Canh Minh Do, Kazuhiro Ogata
Mathematics, 9, 4, 1-16, 2021
Graphical Animations of the NS(L)PK Authentication Protocols.
Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, Canh Minh Do, Kazuhiro Ogata 0001
Journal of Visual Language and Computing, 2021, 2, 39-51, 2021
A Divide & Conquer Approach to Conditional Stable Model Checking
Yati Phyo, Canh Minh Do, Kazuhiro Ogata
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 12819 LNCS, 105-111, 2021
A Parallel Stratified Model Checking Technique/Tool for Leads-to Properties
Canh Minh Do, Yati Phyo, Adrian Riesco, Kazuhiro Ogata
Proceedings - 2021 7th International Symposium on System and Software Reliability, ISSSR 2021, 155-166, 2021
Formal verification of multitask hybrid systems by the OTS/CafeOBJ method.
Masaki Nakamura 0001, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata 0001
SEKE, 114-119, 2021
Formal Verification of Multitask Hybrid Systems by the OTS/CafeOBJ Method.
Masaki Nakamura 0001, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata 0001
International Journal of Software Engineering and Knowledge Engineering, 31, 11&12, 1541-1559, 2021
Parallel stratified random testing for concurrent programs
Canh Minh Do, Kazuhiro Ogata
Proceedings - Companion of the 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS-C 2020, 79-86, 2020
A divide & conquer approach to testing concurrent programs with JPF
Canh Minh Do, Kazuhiro Ogata
Proceedings - Asia-Pacific Software Engineering Conference, APSEC, 2020-December, 356-364, 2020
Stability of termination and sufficient-completeness under pushouts via amalgamation
Daniel Găină, Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
Theoretical Computer Science, -, 2020
Formal verification of Fischer's real-time mutual exclusion protocol by the OTS/CafeOBJ method.
Masaki Nakamura 0001, Shuki Higashi, Kazutoshi Sakakibara, Kazuhiro Ogata 0001
59th Annual Conference of the Society of Instrument and Control Engineers of Japan(SICE), 1210-1215, 2020
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
Toward development of a tool supporting a 2-layer divide & conquer approach to leads-to model checking
Yati Phyo, Canh Minh Do, Kazuhiro Ogata
2019 INTERNATIONAL CONFERENCE ON ADVANCED INFORMATION TECHNOLOGIES (ICAIT), 250-255, 2019
An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms.
Ha Thi Thu Doan, Adrián Riesco 0001, Kazuhiro Ogata 0001
Stabilization, Safety, and Security of Distributed Systems - 21st International Symposium(SSS), 111-126, 2019
Formal Specification and Model Checking of a Ride-sharing System in Maude.
Eiichi Muramoto, Kazuhiro Ogata 0001, Yoichi Shinoda
Structured Object-Oriented Formal Language and Method - 9th International Workshop(SOFL+MSVL), 187-204, 2019
A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and Maude.
Canh Minh Do, Kazuhiro Ogata 0001
Structured Object-Oriented Formal Language and Method - 9th International Workshop(SOFL+MSVL), 42-58, 2019
KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs.
Jiaqi Qian, Min Zhang 0002, Yi Wang, Kazuhiro Ogata 0001
Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software(FASE), 299-305, 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
COMPUTING AND INFORMATICS, 38, 5, 1009-1038, 2019
Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol
Dang Duy Bui, Kazuhiro Ogata
Journal of Visual Language and Computing, -, 2019
Formal Specification and Model Checking of A* Algorithm.
Kazuhiro Ogata 0001
31st International Conference on Software Engineering and Knowledge Engineering (31st SEKE), 181-244, 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 0001
31st International Conference on Software Engineering and Knowledge Engineering (31st SEKE), 159-208, 2019
Specification-based Testing with Simulation Relations (S).
Canh Minh Do, Kazuhiro Ogata 0001
31st International Conference on Software Engineering and Knowledge Engineering (31st SEKE), 107-146, 2019
Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol.
Dang Duy Bui, Kazuhiro Ogata 0001
25th International DMS Conference on Visualization and Visual Languages, 125-137, 2019
GUESSING, MODEL CHECKING AND THEOREM PROVING OF STATE MACHINE PROPERTIES – A CASE STUDY ON QLOCK
May Thu Aung, Tam Thi Thanh Nguyen, Kazuhiro Ogata
International Journal of Software Engineering and Computer Systems, 4, 2, 1-18, 2018
Graphically Perceiving Characteristics of the MCS Lock and Model Checking Them
Tam Thi Thanh Nguyen, Kazuhiro Ogata
STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, SOFL+MSVL 2017, 10795, 3-23, 2018
A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler
Dorian Daudier, Trinh Ngoc Quoc Bao, Kazuhiro Ogata
STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, SOFL+MSVL 2017, 10795, 200-217, 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 Than Nguyen, Kazuhiro Ogata
PROCEEDINGS OF 2018 7TH INTERNATIONAL CONFERENCE ON SOFTWARE AND COMPUTER APPLICATIONS (ICSCA 2018), 153-157, 2018
Analysis of Two Flawed Versions of A Mutual Exclusion Protocol with Maude and SMGA
May Thu Aung, Tam Thi Than Nguyen, Kazuhiro Ogata
PROCEEDINGS OF 2018 7TH INTERNATIONAL CONFERENCE ON SOFTWARE AND COMPUTER APPLICATIONS (ICSCA 2018), 194-198, 2018
Model Checking of the Suzuki-Kasami Distributed Mutual Exclusion Algorithm with SPIN
Shouki Sakamoto, Kazuhiro Ogata
2018 5TH INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND THEIR APPLICATIONS (DSA), 136-141, 2018
Analysis of Some Variants of the Anderson Array-based Queuing Mutual Exclusion Protocol with Model Checking and Graphical Animations
Yati Phyo, Kazuhiro Ogata
2018 5TH INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND THEIR APPLICATIONS (DSA), 126-135, 2018
Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks
Yati Phyo, Kazuhiro Ogata
2018 25TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2018), 89-98, 2018
Model Checking of Robot Gathering
Ha Thi Thu Doan, Francois Bonnet, Kazuhiro Ogata
21st International Conference on Principles of Distributed Systems (21st OPODIS), -, 2017
Model checking the iKP electronic payment protocols
Kazuhiro Ogata
JOURNAL OF INFORMATION SECURITY AND APPLICATIONS, 36, 101-111, 2017
Model Checking of a Mobile Robots Perpetual Exploration Algorithm
Ha Thi Thu Doan, Francois Bonnet, Kazuhiro Ogata
STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, 10189, 201-219, 2017
A Formal Proof Generator from Semi-formal Proof Documents
Adrian Riesco, Kazuhiro Ogata
THEORETICAL ASPECTS OF COMPUTING - ICTAC 2017, 10580, 3-12, 2017
A Way to Comprehend Counterexamples Generated by the Maude LTL Model Checker
Tam Thi Thanh Nguyen, Kazuhiro Ogata
2017 ANNUAL CONFERENCE ON SOFTWARE ANALYSIS, TESTING AND EVOLUTION (SATE 2017), 53-62, 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
Writing concurrent Java programs based on CafeOBJ specifications
Xuan-Linh Ha, Kazuhiro Ogata
2017 24TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2017), 618-623, 2017
Formal modeling and analysis of time- and resource-sensitive simple business processes
Kazuhiro Ogata, Thapana Chaimanont, Min Zhang
JOURNAL OF INFORMATION SECURITY AND APPLICATIONS, 31, 23-40, 2016
CafeInMaude: A CafeOBJ Interpreter in Maude
Adrian Riesco, Kazuhiro Ogata, Kokichi Futatsugi
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2016), 9633, 377-380, 2016
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
Formal Modeling and Analysis of Time- and Resource-sensitive Simple Business Processes
Kazuhiro Ogata, Thapana Chaimanont, Min Zhang
2015 2ND INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING AND INTERNET OF THINGS (DCIT), 1-10, 2015
Model Checking Chandy-Lamport Distributed Snapshot Algorithm Revisited
Ha Thi Thu Doan, Wenjie Zhang, Kazuhiro Ogata, Min Zhang
2015 2ND INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING AND INTERNET OF THINGS (DCIT), 30-39, 2015
Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
2015 22ND ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2015), 159-166, 2015
Liveness Properties in CafeOBJ - A Case Study for Meta-Level Specifications
Norbert Preining, Kazuhiro Ogata, Kokichi Futatsugi
LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2014), 8981, 182-198, 2015
TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned
Iakovos Ouranos, Kazuhiro Ogata, Petros Stefaneas
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E97D, 5, 1160-1170, 2014
On Automation of OTS/CafeOBJ Method
Daniel Gaina, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi
Lecture Notes in Computer Science, 8373, 578, 25-, 2014
A Formal Semantics of the OSEK/VDX Standard in K Framework and Its Applications
Min Zhang, Yunja Choi, Kazuhiro Ogata
REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2014, 8663, 280-296, 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
Special Section on Formal Approach FOREWORD
Kazuhiro Ogata
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E96D, 6, 1257-1257, 2013
Incremental proofs of operational termination with modular conditional dependency pairs
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
Lecture Notes in Engineering and Computer Science, 2202, 516-521, 2013
On Proving Operational Termination Incrementally with Modular Conditional Dependency Pairs
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
IAENG International Journal of Computer Science,, 40, 2, 117-123, 2013
Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method
Kazuhiro Ogata, Kokichi Futatsugi
JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 19, 6, 771-804, 2013
A Divide & Conquer Approach to Model Checking of Liveness Properties
Kazuhiro Ogata, Min Zhang
2013 IEEE 37TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 648-657, 2013
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
Model Checking Liveness Properties under Fairness & Anti-fairness Assumptions
Kazuhiro Ogata
2013 20TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2013), VOL 1, 1, 565-570, 2013
On Describing Terminating Algebraic Specifications Based on Their Models
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
INTERNATIONAL MULTICONFERENCE OF ENGINEERS AND COMPUTER SCIENTISTS, IMECS 2012, VOL I, 269-274, 2012
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
Invariant-preserved Transformation of State Machines from Equations into Rewrite Rules
Min Zhang, Kazuhiro Ogata
2012 19TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), VOL 1, 511-516, 2012
An Algebraic Approach to Formal Analysis of Dynamic Software Updating Mechanisms
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi
2012 19TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), VOL 1, 664-673, 2012
Constructor-based Logics
Daniel Gaina, Kokichi Futatsugi, Kazuhiro Ogata
JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 18, 16, 2204-2233, 2012
Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support
Min Zhang, Kazuhiro Ogata, Masaki Nakamura
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E94D, 5, 976-988, 2011
Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
JOURNAL OF SYMBOLIC COMPUTATION, 45, 5, 551-573, 2010
Towards Reliable E-Government Systems with the OTS/CafeOBJ Method
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E93D, 5, 974-984, 2010
Specification Translation of State Machines from Equational Theories into Rewrite Theories
Min Zhang, Kazuhiro Ogata, Masaki Nakamura
FORMAL METHODS AND SOFTWARE ENGINEERING, 6447, 678-+, 2010
Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method
Iakovos Ouranos, Petros Stefaneas, Kazuhiro Ogata
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT I, 6415, 75-+, 2010
A Combination of Forward and Backward Reachability Analysis Methods
Kazuhiro Ogata, Kokichi Futatsugi
FORMAL METHODS AND SOFTWARE ENGINEERING, 6447, 501-517, 2010
User-Defined On-Demand Matching
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E92D, 7, 1401-1411, 2009
Introducing CafeOBJ (6) : Verification of a Communication Protocol
OGATA Kazuhiro, FUTATSUGI Kokichi, NAKAMURA Masaki
Computer Software, 26, 2, 93-106, 2009
Constructor-Based Institutions
Daniel Gaina, Kokichi Futatsugi, Kazuhiro Ogata
ALGEBRA AND COALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, 5728, 398-412, 2009
Modular Implementation of a Translator from Behavioral Specifications to Rewrite Theory Specifications
Min Zhang, Kazuhiro Ogata
2009 NINTH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC 2009), 406-411, 2009
Introducing CafeOBJ (5) : Verification of an Authentication Protocol
OGATA Kazuhiro, FUTATSUGI Kokichi, NAKAMURA Masaki
Computer Software, 26, 1, 71-83, 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
Proof Score Approach to Verification of Liveness Properties
Kazuhiro Ogata, Kokichi Futatsugi
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E91D, 12, 2804-2817, 2008
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
A specification translation from behavioral specifications to rewrite specifications
Masaki Nakamura, Weiqiang Kong, Kazuhiro Gata, Kokichi Futatsugi
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, E91D, 5, 1492-1503, 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
Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes
Kazuhiro Ogata, Kokichi Futatsugi
FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 5256, 187-206, 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
Verifying design with proof scores
Kokichi Futatsugi, Joseph A. Goguen, Kazuhiro Ogata
VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 4171, 277-+, 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
Comparison of Maude and SAL by conducting case studies model checking a distributed algorithm
Kazuhiro Ogata, Kokichi Futatsugi
IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, E90A, 8, 1690-1703, 2007
Specification and verification of workflows with RBAC mechanism and SoD constraints
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 17, 1, 3-32, 2007
From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ
Xiang Jianwen, Ogata Kazuhiro, Kong Weiqiang, Futatsugi Kokichi
Information and Media Technologies, 2, 2, 448-460, 2007
Algebraic approaches to formal analysis of the Mondex electronic purse system
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
INTEGRATED FORMAL METHODS, PROCEEDINGS, 4591, 393-412, 2007
A toolkit for generating and displaying proof scores in the OTS/CafeOBJ method
Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
Electronic Notes in Theoretical Computer Science, 147, 1, 57-72, 2006
From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ
Xiang Jianwen, Ogata Kazuhiro, Kong Weiqiang, Futatsugi Kokichi
Computer Software, 23, 3, 134-146, 2006
Induction-guided falsification
Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi
FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 4260, 114-131, 2006
Automating invariant verification of behavioral specifications
Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, Kokichi Futatsugi
QSIC 2006: SIXTH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE, PROCEEDINGS, 49-+, 2006
Reducible Operation Symbols for the Term Rewriting System and Their Applications
NAKAMURA MASAKI, OGATA KAZUHIRO, FUTATSUGI KOKICHI
情報処理学会論文誌プログラミング(PRO), 46, 6, 47-59, 2005
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
A lightweight integration of theorem proving and model checking for system verification
Weiqiang Kong, Kazuhiro Ogata, Takahiro Seino, Kokichi Futatsugi
Proceedings - Asia-Pacific Software Engineering Conference, APSEC, 2005, 59-66, 2005
Analysis of the Suzuki-Kasami algorithm with SAL model checkers
Kazuhiro Ogata, Kokichi Futatsugi
Proceedings - Fifth International Conference on Computer and Information Technology, CIT 2005, 2005, 937-943, 2005
Analysis of the Suzuki-Kasami algorithm with the Maude model checker
Kazuhiro Ogata, Kokichi Futatsugi
Proceedings - Asia-Pacific Software Engineering Conference, APSEC, 2005, 159-166, 2005
Formal fault tree analysis of state transition systems
Jianwen Xiang, Kazuhiro Ogata, Kokichi Futatsugi
Proceedings - International Conference on Quality Software, 2005, 124-131, 2005
Formal Analysis of Workflow Systems with Security Considerations
Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
17th International Conference on Software Engineering and Knowledge Engineering (17th SEKE), 531-536, 2005
Analysis of Positive Incentives for Protecting Secrets in Digital Rights Management
Jianwen Xiang, Weiqiang Kong, Kokichi Futatsugi, Kazuhiro Ogata
2nd International Conference on Web Information Systems and Technologies (2nd WEBIST), 124-131, 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
Chocolat/SMV: A translator from CafeOBJ into SMV
K Ogata, M Nakano, M Nakamura, K Futatsugi
PDCAT 2005: Sixth International Conference on Parallel and Distributed Computing, Applications and Technologies, Proceedings, 416-420, 2005
Rewriting-Based Verification of Authentication Protocols
Kazuhiro Ogata, Kokichi Futatsugi
Electronic Notes in Theoretical Computer Science, 71, 208-222, 2004
書き換えによるOtway-Rees認証プロトコルの検証
清野貴博, 加藤淳, 緒方和博
第11回ソフトウェア工学の基礎ワークショップ(第11回FOSE), 153-156, 2004
SMVによるOTS/CafeOBJ仕様のモデル検査
中野昌弘, 中村正樹, 緒方和博, 二木厚吉
第11回ソフトウェア工学の基礎ワークショップ(第11回FOSE), 129-140, 2004
Falsification of OTSs by Searches of Bounded Reachable State Spaces
Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi
18th International Conference on Software Engineering and Knowledge Engineering (18th SEKE),, 440-445, 2004
Formal Analysis of the NetBill Electronic Commerce Protocol
Kazuhiro Ogata, Kokichi Futatsugi
Lecture Notes in Computer Science, 3233, 45-64, 2004
Formal analysis of an anonymous fair exchange E-commerce protocol
Weiqiang Kong, K. Ogata, Jianwen Xiang, K. Futatsugi
The Fourth International Conference onComputer and Information Technology, 2004. CIT '04., -, 2004
Equational approach to formal verification of SET
Kazuhiro Ogata, Kokichi Futatsugi
Proceedings - Fourth International Conference on Quality Software, QSIC 2004, 50-59, 2004
Modeling and Verification of Hybrid Systems Based on Equations
Kazuhiro Ogata, Daigo Yamagishi, Takahiro Seino, Kokichi Futatsugi
IFIP International Federation for Information Processing, 43-52, 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
Supporting case analysis with algebraic speci .cation languages
T. Seino, K. Ogata, K. Futatsugi
The Fourth International Conference onComputer and Information Technology, 2004. CIT '04., -, 2003
Formal Analysis of the iKP Electronic Payment Protocols
Kazuhiro Ogata, Kokichi Futatsugi
Software Security — Theories and Systems, 441-460, 2003
Formal Verification of the Horn-Preneel Micropayment Protocol
Kazuhiro Ogata, Kokichi Futatsugi
Lecture Notes in Computer Science, 238-252, 2003
Organizing case analysis for verifying safety properties with term rewriting
SEINO Takahiro, OGATA Kazuhiro, FUTATSUGI Kokichi
Computer Software, 20, 5, 444-457, 2003
CafeOBJ: Logical foundations and methodologies
R Diaconescu, K Futatsugi, K Ogata
COMPUTING AND INFORMATICS, 22, 3-4, 257-283, 2003
項書換えを用いた安全性検証の組織化
清野貴博, 緒方和博, 二木厚吉
第9回ソフトウェア工学の基礎ワークショップ(第9回FOSE), 107-118, 2002
Proof Score Approach to Verification of Liveness Properties
Kazuhiro Ogata, Kokichi Futatsugi
17th International Conference on Software Engineering and Knowledge Engineering (17th SEKE), 608-613, 2002
Specification and verification of a single-track railroad signaling in CafeOBJ
T Seino, K Ogata, K Futatsugi
IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, E84A, 6, 1471-1478, 2001
Specification and verification of tokenless blocking systems with CafeOBJ
Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi
2001 International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2001), 807-811, 2001
実時間制約を考慮したマルチタスキングのモデル化
清野貴博, 緒方和博, 二木厚吉, 日比野靖
第8回ソフトウェア工学の基礎ワークショップ(第8回FOSE), 143-146, 2001
Formally modeling and verifying Ricart & Agrawala distributed mutual exclusion algorithm
Kazuhiro Ogata, Kokichi Futatsugi
Proceedings - 2nd Asia-Pacific Conference on Quality Software, APAQS 2001, 357-366, 2001
Specifying and verifying a railroad crossing with cafeOBJ
K. Ogata, K. Futatsugi
Proceedings - 15th International Parallel and Distributed Processing Symposium, IPDPS 2001, 1526-1533, 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
Formal analysis of Suzuki&Kasami distributed mutual exclusion algorithm
Kazuhiro Ogata, Kokichi Futatsugi
IFIP TC6/WG6.1 5th International Conference on Formal Methods for Open Object-Based Distributed Systems (5th FMOODS), 181-195, 2000
The evaluation strategy for head normal form with and without on-demand flags
Masaki Nakamura, Kazuhiro Ogata
Electronic Notes in Theoretical Computer Science, 36, 212-228, 2000
Operational semantics of rewriting with the on-demand evaluation strategy
Kazuhiro Ogata, Kokichi Futatsugi
Proceedings of the ACM Symposium on Applied Computing, 2, 756-763, 2000
代数仕様言語CafeOBJによる鉄道信号システムの記述と検証
清野貴博, 緒方和博, 二木厚吉
第6回ソフトウェア工学の基礎ワークショップ(第6回FOSE), 180-187, 1999
Formal verification of the MCS list-based queuing lock
Kazuhiro Ogata, Kokichi Futatsugi
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 1742, 281-293, 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
Optimizing term rewriting using discrimination nets with specialization
Kazuhiro Ogata, Shigenori Ioroi, Kokichi Futatsugi
Proceedings of the 1999 ACM symposium on Applied computing - SAC '99, -, 1999
CafeOBJのモジュールシステムの設計およびCafeOBJによる検証
五百蔵重典, 緒方和博, 二木厚吉
第5回ソフトウェア工学の基礎ワークショップ(第5回FOSE), 209-218, 1998
Experimental implementation of parallel TRAM on massively parallel computer
Kazuhiro Ogata, Hiromichi Hirata, Shigenori Ioroi, Kokichi Futatsugi
Euro-Par’98 Parallel Processing, 846-851, 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
Design and implementation of parallel TRAM
Kazuhiro Ogata, Masaru Kondo, Shigenori Ioroi, Kokichi Futatsugi
Euro-Par'97 Parallel Processing, 1209-1216, 1997
Implementation of term rewritings with the evaluation strategy
Kazuhiro Ogata, Kokichi Futatsugi
Lecture Notes in Computer Science, 225-239, 1997
TRAM: An abstract machine for order-sorted conditional term rewriting systems
Kazuhiro Ogata, Koichi Ohhara, Kokichi Futatsugi
Rewriting Techniques and Applications, 335-338, 1997
項の構造を考慮したAC照合
五百蔵重典, 緒方和博, 二木厚吉
第3回ソフトウェア工学の基礎ワークショップ(第3回FOSE), 106-109, 1996
Object allocation and dynamic compilation in multithreadsmalltalk
Kazuhiro Ogata, Norihisa Doi
Proceedings of the ACM Symposium on Applied Computing, 129433, 452-456, 1994
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
Knowledge representation and inference - an approach from object-oriented computing and fuzzy theory -
Kazuhiro Ogata, Norihisa Doi
1st Pacific Rim International Conference on Artificial Intelligence (1st PRICAI), 729-734, 1990