default search action
Kazuhiro Ogata 0001
Person information
- affiliation: Japan Advanced Institute of Science and Technology (JAIST), Nomi, Japan
- affiliation (PhD 1995): Keio University, Yokohama, Japan
Other persons with the same name
- Kazuhiro Ogata 0002 — Tokushima University, Electrical and Electronic Engineering, Japan
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j56]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: 1672-1687 (2024) - [j55]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): 36865-36898 (2024) - [j54]Canh Minh Do, Kazuhiro Ogata:
Symbolic model checking quantum circuits in Maude. PeerJ Comput. Sci. 10: e2098 (2024) - [c123]Duong Dinh Tran, Kazuhiro Ogata:
Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ. WRLA 2024: 45-61 - [c122]Canh Minh Do, Kazuhiro Ogata:
Equivalence Checking of Quantum Circuits Based on Dirac Notation in Maude. WRLA 2024: 84-103 - [e4]Kazuhiro Ogata, Narciso Martí-Oliet:
Rewriting Logic and Its Applications - 15th International Workshop, WRLA 2024, Luxembourg City, Luxembourg, April 6-7, 2024, Revised Selected Papers. Lecture Notes in Computer Science 14953, Springer 2024, ISBN 978-3-031-65940-9 [contents] - 2023
- [j53]Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani:
Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude. IET Inf. Secur. 2023: 1-17 (2023) - [j52]Yati Phyo, Moe Nandi Aung, Canh Minh Do, Kazuhiro Ogata:
A Layered and Parallelized Method of Eventual Model Checking. Inf. 14(7): 384 (2023) - [j51]Dang Duy Bui, Minxuan Liu, Duong Ding Tran, Kazuhiro Ogata:
Graphical Animations of an Autonomous Vehicle Merging Protocol. J. Vis. Lang. Comput. 2023(1): 9-24 (2023) - [j50]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: e1284 (2023) - [j49]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: e1547 (2023) - [j48]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: e1556 (2023) - [j47]Min Zhang, Kazuhiro Ogata:
Selected papers from the 15th international symposium on Theoretical Aspects of Software Engineering (TASE 2021). Sci. Comput. Program. 225: 102912 (2023) - [j46]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): 151:1-151:38 (2023) - [c121]Tsubasa Takagi, Canh Minh Do, Kazuhiro Ogata:
Automated Quantum Program Verification in Dynamic Quantum Logic. DaLí 2023: 68-84 - [c120]Takanori Ishibashi, Kazuhiro Ogata:
Formal Specification and Model Checking of Raft Log Replication in Maude. DMSVIVA 2023: 1-6 - [c119]Takanori Ishibashi, Kazuhiro Ogata:
Formal Specification and Model Checking of Raft Leader Election in Maude. ICSCA 2023: 41-45 - [c118]Naomi Okumura, Kazuhiro Ogata:
A way to find counterexamples located at deep positions with domain knowledge of authentication protocols. ICSCA 2023: 206-211 - [c117]Canh Minh Do, Kazuhiro Ogata:
Symbolic Model Checking Quantum Circuits in Maude. SEKE 2023: 103-108 - 2022
- [j45]Canh Minh Do, Kazuhiro Ogata:
Parallel Specification-Based Testing for Concurrent Programs. IEEE Access 10: 24955-24975 (2022) - [j44]Canh Minh Do, Yati Phyo, Kazuhiro Ogata:
Sequential and Parallel Tools for Model Checking Conditional Stable Properties in a Layered Way. IEEE Access 10: 133749-133765 (2022) - [j43]Yati Phyo, Canh Minh Do, Kazuhiro Ogata:
A Divide & Conquer Approach to Leads-to Model Checking. Comput. J. 65(6): 1353-1364 (2022) - [j42]Ha Thi Thu Doan, Kazuhiro Ogata:
Specifying and Model Checking Distributed Control Algorithms at Meta-level. Comput. J. 65(12): 2998-3019 (2022) - [j41]Duong Dinh Tran, Kazuhiro Ogata:
Formal verification of TLS 1.2 by automatically generating proof scores. Comput. Secur. 123: 102909 (2022) - [j40]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. 105-A(5): 823-832 (2022) - [j39]Adrián Riesco, Kazuhiro Ogata:
An integrated tool set for verifying CafeOBJ specifications. J. Syst. Softw. 189: 111302 (2022) - [j38]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): 1-15 (2022) - [j37]Dang Duy Bui, Kazuhiro Ogata:
Better state pictures facilitating state machine characteristic conjecture. Multim. Tools Appl. 81(1): 237-272 (2022) - [c116]Duong Dinh Tran, Kazuhiro Ogata:
IPSG: Invariant Proof Score Generator. COMPSAC 2022: 1050-1055 - [c115]Minxuan Liu, Kazuhiro Ogata, Dang Duy Bui:
Graphical Animations of an Autonomous Vehicle Merging Protocol. DMSVIVA 2022: 16-22 - [c114]Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata, Adrián Riesco:
Integration of SMGA and Maude to Facilitate Characteristic Conjecture. DMSVIVA 2022: 45-54 - [c113]Moe Nandi Aung, Yati Phyo, Canh Minh Do, Kazuhiro Ogata:
A Tool for Model Checking Eventual Model Checking in a Stratified Way. DSA 2022: 270-279 - [c112]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: 16-31 - [c111]Víctor García, Santiago Escobar, Kazuhiro Ogata:
Modeling and verification of the post-quantum key encapsulation mechanism KYBER using Maude. FAVPQC@ICFEM 2022: 32-49 - [c110]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: 50-64 - [c109]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: 382-387 - [c108]Canh Minh Do, Yati Phyo, Kazuhiro Ogata:
A divide and conquer approach to until and until stable model checking. SEKE 2022: 388-393 - [c107]Canh Minh Do, Adrián Riesco, Santiago Escobar, Kazuhiro Ogata:
Parallel Maude-NPA for Cryptographic Protocol Analysis. WRLA@ETAPS 2022: 253-273 - [e3]Sedat Akleylek, Santiago Escobar, Kazuhiro Ogata, Ayoub Otmani:
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. CEUR Workshop Proceedings 3280, CEUR-WS.org 2022 [contents] - 2021
- [j36]Duong Dinh Tran, Dang Duy Bui, Kazuhiro Ogata:
Simulation-Based Invariant Verification Technique for the OTS/CafeOBJ Method. IEEE Access 9: 93847-93870 (2021) - [j35]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): 1541-1559 (2021) - [j34]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): 39-51 (2021) - [c106]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: 854-863 - [c105]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: 22-28 - [c104]Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata:
Graphical Animations of the NSLPK Authentication Protocol (S). DMSVIVA 2021: 29-35 - [c103]Yati Phyo, Canh Minh Do, Kazuhiro Ogata:
A Divide & Conquer Approach to Conditional Stable Model Checking. ICTAC 2021: 105-111 - [c102]Minxuan Liu, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata:
Formal Specification and Model Checking of an Autonomous Vehicle Merging Protocol. QRS Companion 2021: 333-342 - [c101]Masaki Nakamura, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata:
Formal verification of multitask hybrid systems by the OTS/CafeOBJ method. SEKE 2021: 114-119 - [c100]Thet Wai Mon, Shuho Fujii, Duong Dinh Tran, Kazuhiro Ogata:
Formal verification of IFF and NSLPK authentication protocols with CiMPG (S). SEKE 2021: 120-125 - [c99]Naoki Asae, Duong Dinh Tran, Kazuhiro Ogata:
Formal verification of Anderson mutual exclusion protocol by introducing an auxiliary variable (S). SEKE 2021: 126-131 - [c98]Duong Dinh Tran, Kentaro Waki, Kazuhiro Ogata:
Formal specification and model checking of a recoverable wait-free version of MCS. SEKE 2021: 138-143 - 2020
- [j33]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): 1481-1523 (2020) - [j32]Naomi Okumura, Kazuhiro Ogata, Yoichi Shinoda:
Formal analysis of RFC 8120 authentication protocol for HTTP under different assumptions. J. Inf. Secur. Appl. 53: 102529 (2020) - [j31]Daniel Gaina, Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi:
Stability of termination and sufficient-completeness under pushouts via amalgamation. Theor. Comput. Sci. 848: 82-105 (2020) - [c97]Duong Dinh Tran, Dang Duy Bui, Parth Gupta, Kazuhiro Ogata:
Lemma Weakening for State Machine Invariant Proofs. APSEC 2020: 21-30 - [c96]Canh Minh Do, Kazuhiro Ogata:
A divide & conquer approach to testing concurrent programs with JPF*. APSEC 2020: 356-364 - [c95]Dang Duy Bui, Kazuhiro Ogata:
Better State Pictures Facilitating State Machine Characteristic Conjecture. DMSVIVA 2020: 7-12 - [c94]Adrián Riesco, Kazuhiro Ogata:
CiMPG+F: A Proof Generator and Fixer-Upper for CafeOBJ Specifications. ICTAC 2020: 64-82 - [c93]Canh Minh Do, Kazuhiro Ogata:
Parallel stratified random testing for concurrent programs. QRS Companion 2020: 79-86 - [c92]Duong Dinh Tran, Kazuhiro Ogata:
Formal verification of an abstract version of Anderson protocol with CafeOBJ, CiMPA and CiMPG. SEKE 2020: 287-292 - [c91]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: 1210-1215 - [i1]Masaki Nakamura, Kazutoshi Sakakibara, Kazuhiro Ogata:
Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method. CoRR abs/2010.15280 (2020)
2010 – 2019
- 2019
- [j30]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): 1009-1038 (2019) - [j29]Kazuhiro Ogata:
A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions. Frontiers Comput. Sci. 13(1): 51-72 (2019) - [j28]Dang Duy Bui, Kazuhiro Ogata:
Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol. J. Vis. Lang. Comput. 2019(2): 105-116 (2019) - [c90]Dang Duy Bui, Kazuhiro Ogata:
Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol. DMSVIVA 2019: 125-137 - [c89]Jiaqi Qian, Min Zhang, Yi Wang, Kazuhiro Ogata:
KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs. FASE 2019: 299-305 - [c88]Canh Minh Do, Kazuhiro Ogata:
Specification-based Testing with Simulation Relations (S). SEKE 2019: 107-146 - [c87]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: 159-208 - [c86]Kazuhiro Ogata:
Formal Specification and Model Checking of A* Algorithm. SEKE 2019: 181-244 - [c85]Canh Minh Do, Kazuhiro Ogata:
A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and Maude. SOFL+MSVL 2019: 42-58 - [c84]Eiichi Muramoto, Kazuhiro Ogata, Yoichi Shinoda:
Formal Specification and Model Checking of a Ride-sharing System in Maude. SOFL+MSVL 2019: 187-204 - [c83]Ha Thi Thu Doan, Adrián Riesco, Kazuhiro Ogata:
An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms. SSS 2019: 111-126 - 2018
- [j27]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: 71-86 (2018) - [j26]Min Zhang, Kazuhiro Ogata:
From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories. Theor. Comput. Sci. 722: 52-75 (2018) - [j25]Adrián Riesco, Kazuhiro Ogata:
Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores. ACM Trans. Softw. Eng. Methodol. 27(2): 6:1-6:32 (2018) - [c82]Yati Phyo, Kazuhiro Ogata:
Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks. APSEC 2018: 89-98 - [c81]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: 126-135 - [c80]Shouki Sakamoto, Kazuhiro Ogata:
Model Checking of the Suzuki-Kasami Distributed Mutual Exclusion Algorithm with SPIN. DSA 2018: 136-141 - [c79]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: 153-157 - [c78]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: 194-198 - 2017
- [j24]Adrián Riesco, Kazuhiro Ogata, Kokichi Futatsugi:
A Maude environment for CafeOBJ. Formal Aspects Comput. 29(2): 309-334 (2017) - [j23]Kazuhiro Ogata:
Model checking the iKP electronic payment protocols. J. Inf. Secur. Appl. 36: 101-111 (2017) - [c77]Xuan-Linh Ha, Kazuhiro Ogata:
Writing Concurrent Java Programs Based on CafeOBJ Specifications. APSEC 2017: 618-623 - [c76]Tam Thi Thanh Nguyen, Kazuhiro Ogata:
Graphical Animations of State Machines. DASC/PiCom/DataCom/CyberSciTech 2017: 604-611 - [c75]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: 1586-1596 - [c74]Adrián Riesco, Kazuhiro Ogata:
A Formal Proof Generator from Semi-formal Proof Documents. ICTAC 2017: 3-12 - [c73]Ha Thi Thu Doan, François Bonnet, Kazuhiro Ogata:
Model Checking of Robot Gathering. OPODIS 2017: 12:1-12:16 - [c72]Tam Thi Thanh Nguyen, Kazuhiro Ogata:
A Way to Comprehend Counterexamples Generated by the Maude LTL Model Checker. SATE 2017: 53-62 - [c71]Tam Thi Thanh Nguyen, Kazuhiro Ogata:
Graphically Perceiving Characteristics of the MCS Lock and Model Checking Them. SOFL+MSVL 2017: 3-23 - [c70]Dorian Daudier, Trinh Ngoc Quoc Bao, Kazuhiro Ogata:
A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler. SOFL+MSVL 2017: 200-217 - 2016
- [j22]Kazuhiro Ogata, Thapana Chaimanont, Min Zhang:
Formal modeling and analysis of time- and resource-sensitive simple business processes. J. Inf. Secur. Appl. 31: 23-40 (2016) - [c69]Adrián Riesco, Kazuhiro Ogata, Kokichi Futatsugi:
CafeInMaude: A CafeOBJ Interpreter in Maude. FASE 2016: 377-380 - [c68]Ha Thi Thu Doan, François Bonnet, Kazuhiro Ogata:
Model Checking of a Mobile Robots Perpetual Exploration Algorithm. SOFL+MSVL 2016: 201-219 - [e2]Kazuhiro Ogata, Mark Lawford, Shaoying Liu:
Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings. Lecture Notes in Computer Science 10009, 2016, ISBN 978-3-319-47845-6 [contents] - 2015
- [c67]Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi:
Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates. APSEC 2015: 159-166 - [c66]Masaki Nakamura, Daniel Gâinâ, Kazuhiro Ogata, Kokichi Futatsugi:
Proving Sufficient Completeness of Constructor-Based Algebraic Specifications. CSA/CUTE 2015: 15-21 - [c65]Hiroyuki Yoshida, Kazuhiro Ogata, Kokichi Futatsugi:
Formalization and Verification of Declarative Cloud Orchestration. ICFEM 2015: 33-49 - [c64]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: 33-47 - 2014
- [j21]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. 97-D(5): 1160-1170 (2014) - [c63]Yunja Choi, Min Zhang, Kazuhiro Ogata:
Evaluation of Maude as a Test Generation Engine for Automotive Operating Systems. APSEC (1) 2014: 295-302 - [c62]Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi:
Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications. Specification, Algebra, and Software 2014: 92-109 - [c61]Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi:
Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method. Specification, Algebra, and Software 2014: 560-577 - [c60]Daniel Gâinâ, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi:
On Automation of OTS/CafeOBJ Method. Specification, Algebra, and Software 2014: 578-602 - [c59]Kazuhiro Ogata, Kokichi Futatsugi:
Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs. Specification, Algebra, and Software 2014: 630-656 - [c58]Norbert Preining, Kazuhiro Ogata, Kokichi Futatsugi:
Liveness Properties in CafeOBJ - A Case Study for Meta-Level Specifications. LOPSTR 2014: 182-198 - [c57]Min Zhang, Yunja Choi, Kazuhiro Ogata:
A Formal Semantics of the OSEK/VDX Standard in $${\mathbb {K}}$$ Framework and Its Applications. WRLA 2014: 280-296 - [e1]Shusaku Iida, José Meseguer, Kazuhiro Ogata:
Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi. Lecture Notes in Computer Science 8373, Springer 2014, ISBN 978-3-642-54623-5 [contents] - 2013
- [j20]Kazuhiro Ogata:
Foreword. IEICE Trans. Inf. Syst. 96-D(6): 1257 (2013) - [j19]Kazuhiro Ogata, Kokichi Futatsugi:
Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method. J. Univers. Comput. Sci. 19(6): 771-804 (2013) - [c56]Kazuhiro Ogata:
Model Checking Liveness Properties under Fairness & Anti-fairness Assumptions. APSEC (1) 2013: 565-570 - [c55]Kazuhiro Ogata, Min Zhang:
A Divide and Conquer Approach to Model Checking of Liveness Properties. COMPSAC 2013: 648-657 - [c54]Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi:
Formalization and Verification of Behavioral Correctness of Dynamic Software Updates. VSSE 2013: 12-23 - 2012
- [j18]Daniel Gâinâ, Kokichi Futatsugi, Kazuhiro Ogata:
Constructor-based Logics. J. Univers. Comput. Sci. 18(16): 2204-2233 (2012) - [j17]Kokichi Futatsugi, Daniel Gâinâ, Kazuhiro Ogata:
Principles of proof scores in CafeOBJ. Theor. Comput. Sci. 464: 90-112 (2012) - [c53]Min Zhang, Kazuhiro Ogata:
Invariant-preserved Transformation of State Machines from Equations into Rewrite Rules. APSEC 2012: 511-516 - [c52]