業績リスト
[国際論文誌論文(全文査読有)]
[1] Takahiro Seino, Kazuhiro Ogata
and Kokichi Futatsugi:
Specification and verification of a single-track railroad signaling in CafeOBJ, IEICE TRANSACTIONS on Fundamental of Electronics,
Communications and Computer Science, E84-A(6): 1471-1478, IEICE, 2001. https://search.ieice.org/bin/summary.php?id=e84-a_6_1471
[2]
Kazuhiro Ogata and Kokichi Futatsugi: Flaw and modification of the iKP electronic payment protocols, Information Processing
Letters, 86(2): 57-62, Elsevier, 2003. https://doi.org/10.1016/S0020-0190(02)00480-5
[3]
Razvan Diaconescu, Kokichi Futatsugi and Kazuhiro
Ogata: CafeOBJ: Logical Foundation and
Methodologies, Computing and Informatics, 22(3): 257-283, Slovak Academic Press,
2003. https://www.sav.sk/index.php?lang=en&doc=journal-list&part=article_response_page&journal_article_no=14
[4]
Takahiro Seino, Kazuhiro Ogata and Kokichi
Futatsugi: Mechanically Supporting Case Analysis for
Verification of Distributed Systems, International Journal of Pervasive
Computing and Communications, 1(2): 135-145, Emerald, 2005. https://doi.org/10.1108/17427370580000119
[5] Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi: Specification
and Verification of Workflows with RBAC Mechanism and SoD Constraints, International Journal of Software
Engineering and Knowledge Engineering, 17(1): 3-32, World Scientific, 2007. https://doi.org/10.1142/S0218194007003124
[6]
Kazuhiro Ogata and Kokichi Futatsugi: Modeling and verification of real-time systems
based on equations, Science of Computer Programming, 66(2): 162-180, Elsevier,
2007. https://doi.org/10.1016/j.scico.2006.10.011
[7]
Kazuhiro Ogata and Kokichi Futatsugi: Comparison of Maude and SAL by Conducting Case
Studies Model Checking a Distributed Algorithm, IEICE TRANSACTIONS on
Fundamental of Electronics, Communications and Computer Science, E90-A(8):
1690-1703, IEICE, 2007. https://doi.org/10.1093/ietfec/e90-a.8.1690
[8]
Kazuhiro Ogata and Kokichi Futatsugi: State Machines as Inductive Types, IEICE
TRANSACTIONS on Fundamental of Electronics, Communications and Computer Science,
E90-A(12): 2985-2988, IEICE, 2007. https://doi.org/10.1093/ietfec/e90-a.12.2985
[9]
Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura and Kokichi Futatsugi: Creme: An Automatic Invariant Prover of Behavioral
Specifications, International Journal of Software Engineering and Knowledge
Engineering, 17(6): 783-804, World Scientific, 2007. https://doi.org/10.1142/S0218194007003458
[10]
Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata
and Kokichi Futatsugi: A
Specification Translation from Behavioral Specifications to Rewrite
Specifications, IEICE TRANSACTIONS on Information and Systems, E91-D(5):
1492-1503, IEICE, 2008. https://doi.org/10.1093/ietisy/e91-d.5.1492
[11]
Kazuhiro Ogata and Kokichi Futatsugi: Proof Score Approach to Verification of Liveness
Properties, IEICE TRANSACTIONS on Information and Systems, E91-D(12): 2804-2817,
IEICE, 2008. https://doi.org/10.1093/ietisy/e91-d.12.2804
[12]
Jianwen Xiang, Jing Tian, Kazuhiro Ogata, Kokichi Futatsugi and Akira Mori:
Analysis of membership sharing problem in digital subscription services,
International Journal of Revenue Management, 3(3): 284-306, Inderscience Enterprises Ltd., 2009. http://www.inderscience.com/offer.php?id=27388
[13]
Masaki Nakamura, Kazuhiro Ogata and Kokichi
Futatsugi: User-Defined On-Demand Matching, IEICE
TRANSACTIONS on Information and Systems, E92-D(7): 1401-1411, IEICE, 2009. https://doi.org/10.1587/transinf.E92.D.1401
[14]
Masaki Nakamura, Kazuhiro Ogata and Kokichi
Futatsugi: Reducibility of operation symbols in term
rewriting systems and its application to behavioral specifications, Journal of
Symbolic Computation, 45(5): 551-573, Elsevier, 2010. https://doi.org/10.1016/j.jsc.2010.01.008
[15]
Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi: Towards Reliable E-Government Systems with the OTS/CafeOBJ Method, IEICE TRANSACTIONS on Information and
Systems, E93-D(5): 974-984, IEICE, 2010. https://doi.org/10.1587/transinf.E93.D.974
[16]
Kazuhiro Ogata and Kokichi Futatsugi: Proof Score Approach to Analysis of Electronic
Commerce Protocols, International Journal of Software Engineering and Knowledge
Engineering, 20(2): 253-287, World Scientific, 2010. https://doi.org/10.1142/S0218194010004712
[17]
Min Zhang, Kazuhiro Ogata and Masaki Nakamura: Translation of State
Machines from Equational Theories into Rewrite Theories with Tool Support, IEICE
TRANSACTIONS on Information and Systems, E94-D(5): 976-988, IEICE, 2011. https://doi.org/10.1587/transinf.E94.D.976
[18]
Kokichi Futatsugi, Daniel
Gaina and Kazuhiro Ogata: Principles of proof
scores in CafeOBJ, Theoretical Computer Science (TCS),
464: 90-112, Elsevier, 2012. https://doi.org/10.1016/j.tcs.2012.07.041
[19]
Daniel Gaina, Kokichi Futatsugi and Kazuhiro Ogata: Constructor-based
Logics, The Journal of Universal Computer Science (J. UCS), 18(16): 2204-2233,
J.UCS consortium, 2012. https://doi.org/10.3217/jucs-018-16-2204
[20]
Kazuhiro Ogata, Kokichi Futatsugi: Compositionally Writing Proof Scores of
Invariants in the OTS/CafeOBJ Method, The Journal of
Universal Computer Science (J. UCS), 19(6): 771-804,
J.UCS consortium, 2013. https://doi.org/10.3217/jucs-019-06-0771
[21]
Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi: On Proving Operational Termination Incrementally
with Modular Conditional Dependency Pairs, IAENG International Journal of
Computer Science, 40(2): 117-123, International Association of Engineers
(IAENG), 2013. http://www.iaeng.org/IJCS/issues_v40/issue_2/IJCS_40_2_08.pdf
[22]
Iakovos
Ouranos, Petros Stefaneas, Kazuhiro Ogata: TESLA source
authentication protocol verification experiment in the Timed OTS/CafeOBJ method: Experiences and Lessons Learned,
IEICE TRANSACTIONS on Information and Systems, E97-D(5):
1160-1170, IEICE, 2014. https://doi.org/10.1587/transinf.E97.D.1160
[23]
Kazuhiro Ogata, Thapana Chaimanont, Min Zhang: Formal Modeling and Analysis of Time-
and Resource-sensitive Simple Business Processes, Journal of Information
Security and Applications (JISA), 31: 23-40, Elsevier, 2016. https://doi.org/10.1016/j.jisa.2016.05.001
[24]
Adrian Riesco, Kazuhiro Ogata, Futatsugi Kokichi: A Maude
Environment for CafeOBJ, Formal Aspects of Computing,
Springer (FAoC), 29(2): 309-334, Springer, 2017. https://doi.org/10.1007/s00165-016-0398-7
[25]
Kazuhiro Ogata: A Divide & Conquer Approach to Liveness Model
Checking under Fairness & Anti-fairness Assumptions, Frontiers of Computer
Science (FCS), 13(1): 51-72, Higher Education Press and Springer, 2019.
https://doi.org/10.1007/s11704-017-7036-2
[26]
Kazuhiro Ogata: Model Checking the iKP
Electronic Payment Protocols, Journal of Information Security and Applications
(JISA), 36: 101-111, Elsevier, 2017. https://doi.org/10.1016/j.jisa.2017.08.006
[27]
Min Zhang, Kazuhiro Ogata: From hidden to visible: A unified framework for transforming
behavioral theories into rewrite theories,
Theoretical Computer Science (TCS), 722: 52-75, Elsevier, 2018. https://doi.org/10.1016/j.tcs.2018.01.006
[28]
Adrian Resco, Kazuhiro Ogata:
Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores,
ACM Transactions on Software Engineering and Methodology (ACM TOSEM),
27(2): 6:1-6:32, ACM, 2018. https://doi.org/10.1145/3208951
[29]
Manjukeshwar Reddy Mandadi,
Varuneshwar Reddy Mandadi,
Kazuhiro Ogata: Formal
Analysis of a Security Protocol for e-Passports based on
Rewrite Theory Specifications, Journal
of Information Security and Applications (JISA), 42: 71-86, Elsevier,
2018. https://doi.org/10.1016/j.jisa.2018.08.005
[30]
May Thu Aung, Tam Thi Thanh Nguyen, Kazuhiro
Ogata: Guessing, Model Checking and Theorem Proving of State Machine
Properties –
A Case Study on Qlock, International Journal of
Software Engineering and Computer Systems (IJSECS), 4(2): 1-18, Universiti Malaysia Pahang (UMP) Publisher, 2018. https://doi.org/10.15282/ijsecs.4.2.2018.1.0045
[31]
Dang Duy Bui, Kazuhiro Ogata: Graphical
Animations of the Suzuki-Kasami Distributed Mutual
Exclusion Protocol,
Journal of Visual Language and Computing (JVLC), 2019(2): 105-115, KSI Research
Inc., 2019. https://doi.org/10.18293/JVLC2019-N2-012
[32]
Ha Thi Thu Doan, Kazuhiro Ogata: A More
Faithful Formal Definition of the Desired Property for Distributed Snapshot
Algorithms to Model Check the Property, Computing and Informatics, 38 (5):
1009-1038, Slovak Academic Press,
2019. https://doi.org/10.31577/cai_2019_5_1009
[33]
Naomi Okumura, Kazuhiro Ogata, Yoichi Shinoda: Formal Analysis of RFC
8120 Authentication Protocol for HTTP under Different Assumptions, Journal
of Information Security and Applications (JISA), 53: 102529, Elsevier, 2020. https://doi.org/10.1016/j.jisa.2020.102529
[34]
Daniel Gaina, Masaki Nakamura, Kazuhiro Ogata,
Kokichi Futatsugi: Stability
of termination and sufficient-completeness under pushouts via amalgamation,
Theoretical Computer Science (TCS), 848: 82-105, Elsevier, 2020. https://doi.org/10.1016/j.tcs.2020.09.024
[35]
Kazuhiro Ogata: A Generic Approach on How to Formally Specify and Model
Check Path Finding Algorithms: Dijkstra, A* and LPA*, International
Journal of Software Engineering and Knowledge Engineering, 30(10): 1481-1523,
World Scientific, 2020. https://doi.org/10.1142/S0218194020400215
[36]
Yati Phyo, Canh Do Minh, Kazuhiro Ogata: A Divide & Conquer
Approach to Leads-to Model Checking, The Computer Journal 65 (6): 1353-1364,
Oxford University Press (2022). https://doi.org/10.1093/comjnl/bxaa183
[37]
Moe Nandi Aung, Yati Phyo,
Canh Do Minh, Kazuhiro Ogata: A Divide &
Conquer Approach to Eventual Model Checking, Mathematics 2021, 9, 368. https://doi.org/10.3390/math9040368
[38]
Dang Duy Bui, Kazuhiro Ogata: Better State
Pictures Facilitating State Machine Characteristic Conjecture, Multimedia Tools
and Applications 81(1): 237-272, Springer (2022) https://doi.org/10.1007/s11042-021-10992-z
[39]
Duong Dinh Tran, Dang Duy Bui, Kazuhiro Ogata:
Simulation-based invariant verification technique for the OTS/CafeOBJ method,
IEEE Access 9: 93847-93870, IEEE, (2021) https://doi.org/10.1109/ACCESS.2021.3093211
[40]
Ha Thi Thu Doan, Kazuhiro Ogata: Specifying and
Model Checking Distributed Control Algorithms at Meta-level, The Computer
Journal, Oxford University Press (2021). https://doi.org/10.1093/comjnl/bxab122
[41]
Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, Canh Minh Do, Kazuhiro
Ogata: Graphical Animations of the NS(L)PK Authentication Protocols, Journal
of Visual Language and Computing (JVLC), 2021(2): 39-51, KSI Research Inc.,
2021. https://doi.org/10.18293/JVLC2021-N2-005
[42]
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, Journal of Visual Language and
Computing (JVLC), 2022(1): 1-15, KSI Research Inc., 2021. https://doi.org/10.18293/JVLC2022-N1-004
[43]
Masaki Nakamura, Shuki Higashi, Kazutoshi Sakakibara, Kazuhiro
Ogata: Specification and verification of multitask real-time systems using
the OTS/CafeOBJ method, IEICE TRANSACTIONS on Fundamental of Electronics,
Communications and Computer Science, E105-A(5): 823-832, IEICE, (2022). https://doi.org/10.1587/transfun.2021MAP0007
[44]
Masaki Nakamura, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata: Formal
verification of multitask hybrid systems by the OTS/CafeOBJ method,
International Journal of Software Engineering and Knowledge Engineering,
31(11&12): 1541-1559, World Scientific, (2021). https://dx.doi.org/10.1142/S0218194021400118
[45]
Canh Minh Do,, Kazuhiro Ogata: Parallel Specification-based Testing for
Concurrent Programs, IEEE Access 10: 24955-24975, IEEE, (2022). https://doi.org/10.1109/ACCESS.2022.3155629
[46]
Adrian Riesco, Kazuhiro Ogata: An integrated
tool set for verifying CafeOBJ specifications, The Journal of Systems &
Software 189: 111302 (1 - 18), Elsevier, (2022). https://doi.org/10.1016/j.jss.2022.111302
[47]
Duong Dinh Tran, Kazuhiro Ogata: Formal verification of TLS 1.2 by
automatically generating proof scores, Computers & Security 123: 102909 (1 -
15), Elsevier, (2022) https://doi.org/10.1016/j.cose.2022.102909
[48]
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,
IEEE, (2022). https://doi.org/10.1109/ACCESS.2022.3230844
[49]
Duong Dinh Tran, 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 Computer Science 9:e1284 (1-25)
PeerJ, (2023) http://dx.doi.org/10.7717/peerj-cs.1284
[50]
Dang Duy Bui, Minxuan Liu, Duong Dinh Tran,
Kazuhiro Ogata: Graphical Animations of an Autonomous Vehicle
Merging Protocol, Journal of Visual Language and Computing (JVLC), 2023(1):
9-24, KSI Research Inc., 2023. https://doi.org/10-18293/JVLC2023-N1-027
[51] Dang Duy Bui, Duong Dinh Tran,
Kazuhiro Ogata, Adrian Riesco: Integration
of State Machine Graphical Animation and Maude to Facilitate Characteristic
Conjecture: an Approach to Lemma Discovery in Theorem Proving, Multimedia Tools
and Applications XX(YY): ZZZ-ZZZ, Springer (2023) https://doi.org/10.1007/s11042-023-15780-5
[52]
Canh Minh Do, Yati Phyo,
Adrian Riesco, Kazuhiro Ogata: Optimization
Techniques for Model Checking Leads-to Properties in a Stratified Way, ACM
Transactions on Software Engineering and Methodology (ACM TOSEM), X(Y): ZZZ-ZZZ,
ACM, 2023. https://doi.org/10.1145/3604610
[53]
Yati Phyo, Moe Nandi Aung,,
Canh Do Minh, Kazuhiro Ogata: A Layered and
Parallelized Method of Eventual Model Checking, Information 2023, 14, 384 https://doi.org/10.3390/info14070384
[国際会議・シンポジウム・ワークショップ論文(全文査読有)]
[1] Kazuhiro Ogata and Norihisa Doi: Knowledge representation and inference - an approach
from object-oriented computing and fuzzy theory -, Proceedings of the 1st
Pacific Rim International Conference on Artificial Intelligence (1st PRICAI),
pp.729-734 (1990). http://www.jaist.ac.jp/~ogata/mypapers/pricai90.pdf
[2]
Kazuhiro Ogata, Satoshi Kurihara, Mikio Inari and Norihisa Doi: HoME: Smalltalk on Mach
environment, Proceedings of the 6th International Conference on Technology of
Object-Oriented Languages and Systems (6th TOOLS), Prentice Hall, pp.153-161
(1991). http://www.jaist.ac.jp/~ogata/mypapers/tools6.pdf
[3]
Kazuhiro Ogata, Satoshi Kurihara, Mikio Inari and Norihisa Doi: The design and implementation of HoME, Proceedings of the ACM SIGPLAN '92 Conference on
Programming Language Design and Implementation (PLDI 1992), SIGPLAN Notices,
Vol.27, No.7, ACM Press, pp.44-54 (1992). https://doi.org/10.1145/143095.143117
[4]
Kazuhiro Ogata and Norihisa Doi: Object allocation and dynamic compilation in MultithreadSmalltalk, Proceedings of the 1994 ACM Symposium
on Applied Computing (SAC 1994), ACM Press, pp.452-456 (1994). https://doi.org/10.1145/326619.326808
[5]
Kazuhiro Ogata, Koichi Ohhara and Kokichi Futatsugi: TRAM: an
abstract machine for order-sorted conditional term rewriting systems,
Proceedings of the 8th International Conference on Rewriting Techniques and
Applications (8th RTA), LNCS 1232, Springer, pp.335-338 (1997). https://doi.org/10.1007/3-540-62950-5_84
[6]
Kazuhiro Ogata and Kokichi Futatsugi: Implementation of term rewritings with the
evaluation strategy, Proceedings of the 9th International Symposium on
Programming Languages, Implementations, Logics, and Programs (9th PLILP), LNCS
1292, Springer, pp.225-239 (1997). https://doi.org/10.1007/BFb0033847
[7]
Kazuhiro Ogata, Masaru Kondo, Shigenori Ioroi
and Kokichi Futatsugi:
Design and implementation of Parallel TRAM, Proceedings of the 3rd International
Euro-Par Conference (3rd Euro-Par), LNCS 1300, Springer, pp.1209-1216 (1997). https://doi.org/10.1007/BFb0002874
[8]
Takashi Nagaya, Michihiro Matsumoto, Kazuhiro Ogata
and Kokichi Futatsugi:
How to give local strategies to function symbols for equality of two
implementations of the E-strategy with and without evaluated flags, Proceedings
of the 3rd Asian Symposium on Computer Mathematics (3rd ASCM), Lanzhou
University Press, pp.71-81 (1998). https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.50.2985&rep=rep1&type=pdf
[9]
Kazuhiro Ogata, Hiromichi Hirata, Shigenori
Ioroi and Kokichi Futatsugi: Experimental implementation of Parallel TRAM on
massively parallel computer, Proceedings of the 4th International Euro-Par
Conference (4th Euro-Par), LNCS 1470, Springer, pp.846-851 (1998). https://doi.org/10.1007/BFb0057939
[10]
Kazuhiro Ogata, Shigenori Ioroi and Kokichi Futatsugi: Optimizing term
rewriting using discrimination nets with specialization, Proceedings of the 1999
ACM Symposium on Applied Computing (SAC 1999), ACM Press, pp.511-518 (1999). https://doi.org/10.1145/298151.298431
[11]
Kazuhiro Ogata and Kokichi Futatsugi: Specification and verification of some classical
mutual exclusion algorithms with CafeOBJ,
Proceedings of the OBJ/CafeOBJ/Maude Workshop at
Formal Methods 1999, Theta, pp.159-177 (1999). http://www.jaist.ac.jp/~ogata/mypapers/fm99-ocmw.pdf
[12]
Kazuhiro Ogata and Kokichi Futatsugi: Formal verification of the MCS list-based queuing
lock, Proceedings of the 5th Asian Computing Science Conference (5th ASIAN),
LNCS 1742, Springer, pp.281-293 (1999). https://doi.org/10.1007/3-540-46674-6_24
[13]
Kazuhiro Ogata and Kokichi Futatsugi: Operational semantics of rewriting with the
on-demand evaluation strategy, Proceedings of the 2000 ACM Symposium on Applied
Computing (SAC 2000), ACM Press, pp.756-763 (2000). https://doi.org/10.1145/338407.338558
[14]
Masaki Nakamura and Kazuhiro Ogata: The evaluation strategy for
head normal form with and without on-demand flags, Proceedings of the 3rd
International Workshop on Rewriting Logic and its Applications (3rd WRLA), ENTCS
36, Elsevier, pp.212-228 (2000). https://doi.org/10.1016/S1571-0661(05)80143-4
[15]
Kazuhiro Ogata and Kokichi Futatsugi: Specifying and verifying a railroad crossing with
CafeOBJ, Proceedings of the 6th International Workshop
on Formal Methods for Parallel Programming: Theory and Applications (6th FMPPTA)
(Part of Proceedings of IPDPS 2001), IEEE Computer Society Press, p.150, (2001).
https://doi.org/10.1109/IPDPS.2001.925137
[16]
Kazuhiro Ogata and Kokichi Futatsugi: Modeling and verification of distributed
real-time systems based on CafeOJB, Proceedings of the
16th International Conference on Automated Software Engineering (16th ASE), IEEE
Computer Society Press, pp.185-192 (2001). https://doi.org/10.1109/ASE.2001.989804
[17]
Kazuhiro Ogata and Kokichi Futatsugi: Formally modeling and verifying Ricart&Agrawala distributed mutual exclusion algorithm,
Proceedings of the 2nd Asia-Pacific Conference on Quality Software (2nd APAQS),
IEEE Computer Society Press, pp.357-366 (2001). https://doi.org/10.1109/APAQS.2001.990041
[18]
Kazuhiro Ogata and Kokichi Futatsugi: Formal analysis of Suzuki&Kasami distributed mutual exclusion algorithm,
Proceedings of the IFIP TC6/WG6.1 5th International Conference on Formal Methods
for Open Object-Based Distributed Systems (5th FMOODS), Kluwer, pp.181-195
(2002). https://doi.org/10.1007/978-0-387-35496-5_13
[19]
Kazuhiro Ogata and Kokichi Futatsugi: Rewriting-based verification of authentication
protocols, Proceedings of the 4th International Workshop on Rewriting Logic and
its Applications (4th WRLA), ENTCS 71, Elsevier, pp.189-203 (2004). https://doi.org/10.1016/S1571-0661(05)82536-8
[20]
Kazuhiro Ogata and Kokichi Futatsugi: Formal verification of the Horn-Preneel micropayment protocol, Proceedings of the 4th
International Conference on Verification, Model Checking, and Abstract
Interpretation (4th VMCAI), LNCS 2575, Springer, pp.238-252 (2003). https://doi.org/10.1007/3-540-36384-X_20
[21]
Kazuhiro Ogata and Kokichi Futatsugi: Formal analysis of the iKP electronic payment protocols, Proceedings of the
1st International Symposium on Software Security (1st ISSS), LNCS 2609 (Hot
Topics, Software Security - Theories and Systems), Springer, pp.441-460 (2003).
https://doi.org/10.1007/3-540-36532-X_25
[22]
Kazuhiro Ogata and Kokichi Futatsugi: Proof Scores in the OTS/CafeOBJ Method, Proceedings of the 6th IFIP WG6.1
International Conference on Formal Methods for Open Object-Based Distributed
Systems (6th FMOODS), LNCS 2884, Springer, pp.170-184 (2003). https://doi.org/10.1007/978-3-540-39958-2_12
[23]
Kazuhiro Ogata, Daigo Yamagishi, Takahiro Seino
and Kokichi Futatsugi:
Modeling and Verification of Hybrid Systems Based on Equations, Proceedings of
the IFIP 18th World Computer Congress TC10 Working Conference on Distributed and
Parallel Embedded Systems (DIPES 2004), Kluwer, pp.43-52 (2004). https://doi.org/10.1007/1-4020-8149-9_5
[24]
Kazuhiro Ogata and Kokichi Futatsugi: Equational Approach to Formal Verification of
SET, Proceedings of the 4th International Conference on Quality Software (4th
QSIC), IEEE Computer Society Press, pp.50-59 (2004). https://doi.org/10.1109/QSIC.2004.1357944
[25]
Takahiro Seino, Kazuhiro Ogata and Kokichi
Futatsugi: Supporting Case Analysis with Algebraic
Specification Languages, Proceedings of the 4th International Conference on
Computer and Information Technology (4th CIT), IEEE Computer Society Press,
pp.1073-1080 (2004). https://doi.org/10.1109/CIT.2004.1357338
[26]
Weiqiang Kong, Kazuhiro Ogata, Jianwen Xiang, Kokichi Futatsugi: Formal Analysis of an Anonymous Fair Exchange
E-Commerce Protocol, Proceedings of the 4th International Conference on Computer
and Information Technology (4th CIT), IEEE Computer Society Press, pp.1100-1107
(2004). https://doi.org/10.1109/CIT.2004.1357342
[27]
Kazuhiro Ogata and Kokichi Futatsugi: Formal Analysis of the NetBill Electronic Commerce Protocol, Proceedings of
the 2nd International Symposium on Software Security (2nd ISSS), LNCS 3233,
Springer, pp.45-64 (2004). https://doi.org/10.1007/978-3-540-37621-7_3
[28]
Takahiro Seino, Kazuhiro Ogata and Kokichi
Futatsugi: A Toolkit for Generating and Displaying
Proof Scores in the OTS/CafeOBJ Method, Proceedings of
the 6th International Workshop on Rule-Based Programming (6th RULE), ENTCS
147(1), Elsevier, pp.57-72 (2006). https://doi.org/10.1016/j.entcs.2005.06.037
[29]
Kazuhiro Ogata and Kokichi Futatsugi: Equational Approach to Formal Analysis of TLS,
Proceedings of the 25th International Conference on Distributed Computing
Systems (25th ICDCS), IEEE Computer Society Press, pp.795-804 (2005). https://doi.org/10.1109/ICDCS.2005.32
[30]
Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi: Formal Analysis
of Workflow Systems with Security Considerations, Proceedings of the 17th
International Conference on Software Engineering and Knowledge Engineering (17th
SEKE), Knowledge Systems Institute, pp.531-536 (2005). http://ksiresearchorg.ipage.com/seke/Proceedings/seke/SEKE2005_Proceedings.pdf
[31]
Kazuhiro Ogata and Kokichi Futatsugi: Proof Score Approach to Verification of Liveness
Properties, Proceedings of the 17th International Conference on Software
Engineering and Knowledge Engineering (17th SEKE), Knowledge Systems Institute,
pp.608-613 (2005). http://ksiresearchorg.ipage.com/seke/Proceedings/seke/SEKE2005_Proceedings.pdf
[32]
Jittisak Senachak, Takahiro
Seino, Kazuhiro Ogata and Kokichi Futatsugi: Provably Correct Translation from CafeOBJ into Java, Proceedings of the 17th International
Conference on Software Engineering and Knowledge Engineering (17th SEKE),
Knowledge Systems Institute, pp.614-619 (2005). http://ksiresearchorg.ipage.com/seke/Proceedings/seke/SEKE2005_Proceedings.pdf
[33]
Jianwen Xiang, Kazuhiro Ogata and Kokichi Futatsugi: Formal Fault
Tree Analysis of State Transition Systems, Prceedings
of the 5th International Conference on Quality Software (5th QSIC), IEEE
Computer Society Press, pp.124-131 (2005). https://doi.org/10.1109/QSIC.2005.3
[34]
Kazuhiro Ogata and Kokichi Futatsugi: Analysis of the Suzuki-Kasami Algorithm with SAL Model Checkers, Proceedings of the
5th International Conference on Computer and Information Technology (5th CIT),
IEEE Computer Society Press, pp.937-943 (2005). https://doi.org/10.1109/CIT.2005.76
[35]
Kazuhiro Ogata, Masahiro Nakano, Masaki Nakamura and Kokichi Futatsugi: Chocolat/SMV: A Translator from CafeOBJ into SMV, Proceedings of the 6th International
Conference on Parallel and Distributed Computing, Applications and Technologies
(6th PDCAT), IEEE Computer Society Press, pp.416-420 (2005). https://doi.org/10.1109/PDCAT.2005.98
[36]
Kazuhiro Ogata and Kokichi Futatsugi: Analysis of the Suzuki-Kasami Algorithm with the Maude Model Checker, Proceedings
of the 12th Asia-Pacific Software Engineering Conference (12th APSEC), IEEE
Computer Society Press, pp.159-166 (2005). https://doi.org/10.1109/APSEC.2005.40
[37]
Weiqiang Kong, Kazuhiro Ogata, Takahiro Seino
and Kokichi Futatsugi: A
Lightweight Integration of Theorem Proving and Model Checking for System
Verification, Proceedings of the 12th Asia-Pacific Software Engineering
Conference (12th APSEC), IEEE Computer Society Press, pp.59-66 (2005). https://doi.org/10.1109/APSEC.2005.9
[38]
Jianwen Xiang, Weiqiang
Kong, Kokichi Futatsugi and
Kazuhiro Ogata: Analysis of Positive Incentives for Protecting Secrets in
Digital Rights Management, Proceeding of the 2nd International Conference on Web
Information Systems and Technologies (2nd WEBIST), INSTICC Press, pp.5-12
(2006). https://www.academia.edu/40623747/Analysis_of_Positive_Incentives_for_Protecting_Secrets_in_Digital_Rights_Management
[39]
Kazuhiro Ogata and Kokichi Futatsugi: Some Tips on Writing Proof Scores in the
OTS/CafeOBJ Method, Proceedings of the Festschrift
Symposium in Honor of Joseph A. Goguen (Algebra,
Meaning, and Computation: Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday), LNCS 4060,
Springer, pp.596-615 (2006). https://doi.org/10.1007/11780274_31
[40]
Kazuhiro Ogata, Weiqiang Kong and Kokichi Futatsugi: Falsification
of OTSs by Searches of Bounded Reachable State Spaces, Proceedings of the 18th
International Conference on Software Engineering and Knowledge Engineering (18th
SEKE), Knowledge Systems Institute, pp.440-445 (2006). http://ksiresearchorg.ipage.com/seke/Proceedings/seke/SEKE2006_Proceedings.pdf
[41]
Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura and Kokichi Futatsugi: Automating
Invariant Verification of Behavioral Specifications, Proceedings of the 6th
International Conference on Quality Software (6th QSIC), IEEE Computer Society
Press, pp.49-56 (2006). https://doi.org/10.1109/QSIC.2006.17
[42]
Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong
and Kokichi Futatsugi:
Induction-Guided Falsification, Prceedings of the
8th International
Conference on Formal Engineering Methods (8th ICFEM), LNCS
4260, Springer, pp.114-131 (2006). https://doi.org/10.1007/11901433_7
[43]
Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi: Algebraic
Approaches to Formal Analysis of the Mondex Electronic
Purse System, Proceedings of the 6th International Conference on Integrated
Formal Methods (6th IFM), LNCS 4591, Springer, pp.393-412 (2007). https://doi.org/10.1007/978-3-540-73210-5_21
[44]
Kazuhiro Ogata and Kokichi Futatsugi: Simulation-based verification for invariant
properties in the OTS/CafeOBJ method, Proceedings of
the 4th International Refinement Workshop (Refine 2007), ENTCS 201, Elsevier,
pp.127-154 (2008). https://doi.org/10.1016/j.entcs.2008.02.018
[45]
Kokichi Futatsugi, Joseph A.
Goguen and Kazuhiro Ogata: Verifying Design
with Proof Scores, Proceedings of the 1st International Conference on Verified
Software: Theories, Tools, Experiments (1st VSTTE), LNCS 4171, Springer,
pp.277-290 (2008). https://doi.org/10.1007/978-3-540-69149-5_30
[46]
Weiqiang Kong, Kazuhiro Ogata, Jian Cheng, and
Kokichi Futatsugi: Trace
Anonymity in the OTS/CafeOBJ Method, Proceedings of
the 8th International Conference on Computer and Information Technology (8th
CIT), IEEE Computer Society Press, pp.754-759 (2008). https://doi.org/10.1109/CIT.2008.4594769
[47]
Kazuhiro Ogata and Kokichi Futatsugi: Formal Analysis of the Bakery Protocol with
Consideration of Nonatomic Reads and Writes,
Proceedings of the 10th International Conference on Formal Engineering Methods
(10th ICFEM), LNCS 5256, Springer, pp.187-206 (2008). https://doi.org/10.1007/978-3-540-88194-0_13
[48]
Daniel Gaina, Kazuhiro Ogata and Kokichi Futatsugi:
Constructor-Based Institutions, Proceedings of the 3rd Conference on Algebra and
Coalgebra in Computer Science (3rd CALCO), LNCS 5728,
Springer, pp.398-412 (2009). https://doi.org/10.1007/978-3-642-03741-2_27
[49]
Min Zhang and Kazuhiro Ogata: Modular Implementation of a Translator from
Behavioral Specification to Rewrite Theory Specification, Proceedings of the 9th
International Conference on Quality Software (9th QSIC), IEEE Computer Society
Press, pp.406-411 (2009). https://doi.org/10.1109/QSIC.2009.60
[50]
Iakovos Ouranos, Petros S. Stefaneas and
Kazuhiro Ogata:
Formal Modeling and Verification of Sensor Network Encryption
Protocol in the OTS/CafeOBJ Method, Proceedings of the
4th International Symposium on Leveraging Applications of Formal Methods,
Verification, and Validation (4th ISoLA), Part I, LNCS
6415, Springer, pp.75-89 (2010). https://doi.org/10.1007/978-3-642-16558-0_9
[51]
Min Zhang, Kazuhiro Ogata and Masaki Nakamura: Specification Translation
of State Machines from Equational Theories into Rewrite Theories, Proceedings of
the 12th International Conference on Formal Engineering Methods (12th ICFEM),
LNCS 6447, Springer, pp.678-693 (2010). https://doi.org/10.1007/978-3-642-16901-4_44
[52]
Kazuhiro Ogata and Kokichi Futatsugi: A Combination of Forward and Backward
Reachability Analysis Methods, Proceedings of the 12th International Conference
on Formal Engineering Methods (12th ICFEM), LNCS 6447, Springer, pp.501-517
(2010). https://doi.org/10.1007/978-3-642-16901-4_33
[53]
Iakovos Ouranos, Petros S. Stefaneas and
Kazuhiro Ogata: Formal Analysis of TESLA Protocol in the Timed OTS/CafeOBJ Method, Proceedings (Part II) of the 5th
International Symposium on Leveraging Applications of Formal Methods,
Verification, and Validation (5th ISoLA), Part I, LNCS
7610, Springer, pp. 126-142 (2012). https://doi.org/10.1007/978-3-642-34032-1_15
[54]
Kazuhiro Ogata and Phan Thi Thanh Huyen: Specification and Model Checking of the Chandy and Lamport Distributed
Snapshot Algorithm in Rewriting Logic, Proceedings of the 14th International
Conference on Formal Engineering Methods (14th ICFEM), LNCS 7635, Springer, pp.
87-102 (2012). https://doi.org/10.1007/978-3-642-34281-3_9
[55]
Min Zhang and Kazuhiro Ogata: Invariant-preserved Transformation of State
Machines from Equations into Rewrite Rules. Proceedings of the 19th Asia-Pacific
Software Engineering Conference (19th APSEC), IEEE, pp.511-516 (2012). https://doi.org/10.1109/APSEC.2012.99
[56]
Min Zhang, Kazuhiro Ogata and Kokichi Futatsugi: An Algebraic Approach to Formal Analysis of
Dynamic Software Updating Mechanisms. Proceedings of the 19th Asia-Pacific
Software Engineering Conference (19th APSEC), IEEE, pp.664-673 (2012). https://doi.org/10.1109/APSEC.2012.100
[57]
Min Zhang, Kazuhiro Ogata and Kokichi Futatsugi: Formalization and Verification of
Behavioral Correctness of Dynamic Software Updates, Proceedings of the 2nd
Workshop on Validation Strategies for Software Evolution (2nd VSSE), ENTCS 294,
Elsevier, pp.12-23 (2013). https://doi.org/10.1016/j.entcs.2013.02.013
[58]
Kazuhiro Ogata and Min Zhang: A Divide & Conquer Approach to Model
Checking of Liveness Properties, Proceedings of the 37th Annual International
Computer Software & Applications Conference (37th COMPSAC), IEEE Computer
Society Press, pp.648-657 (2013). https://doi.org/10.1109/COMPSAC.2013.104
[59]
Kazuhiro Ogata: Model Checking Liveness Properties under Fairness &
Anti-fairness Assumptions, Proceedings of the 20th Asia-Pacific Software
Engineering Conference (20th APSEC), IEEE, pp.565-570 (2013). https://doi.org/10.1109/APSEC.2013.82
[60]
Min
Zhang, Yunja Choi, and Kazuhiro Ogata: A Formal
Semantics of the OSEK/VDX Standard in K Framework and its Applications,
Proceedings of the 10th International Workshop on Rewriting Logic and its
Applications (10th WRLA), LNCS 8663, Springer, pp. 280-296
(2014). https://doi.org/10.1007/978-3-319-12904-4_16
[61]
Masaki
Nakamura, Kazuhiro Ogata, and Kokichi Futatsugi: Incremental Proofs of Termination, Confluence and
Sufficient Completeness of OBJ Specifications, Specification, Algebra, and
Software: Essays Dedicated to Kokichi Futatsugi, LNCS 8373, Springer, pp.92-109 (2014). https://doi.org/10.1007/978-3-642-54624-2_5
[62]
Min
Zhang, Kazuhiro Ogata, and Kokichi Futatsugi: Verifying the Design of Dynamic Software Updating
in the OTS/CafeOBJ Method, Specification, Algebra, and
Software: Essays Dedicated to Kokichi Futatsugi, LNCS 8373, Springer, pp.560-577 (2014). https://doi.org/10.1007/978-3-642-54624-2_28
[63]
Daniel
Gaina, Dorel Lucanu,
Kazuhiro Ogata, and Kokichi Futatsugi: On Automation of OTS/CafeOBJ Method, Specification, Algebra, and Software: Essays
Dedicated to Kokichi Futatsugi, LNCS 8373, Springer, pp.578-602 (2014). https://doi.org/10.1007/978-3-642-54624-2_29
[64]
Kazuhiro
Ogata,
and Kokichi Futatsugi:
Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs,
Specification, Algebra, and Software: Essays Dedicated to Kokichi Futatsugi, LNCS 8373,
Springer, pp.630-656 (2014). https://doi.org/10.1007/978-3-642-54624-2_31
[65]
Yunja Choi, Min Zhang, and Kazuhiro
Ogata:
Evaluation of Maude as a test generation engine for automotive operating
systems, Proceedings of the 21st Asia-Pacific Software Engineering Conference
(21st APSEC), IEEE, pp.295-302 (2014). https://doi.org/10.1109/APSEC.2014.52
[66]
Norbert Preining, Kazuhiro Ogata, and Kokichi Futatsugi: Liveness
Properties in CafeOBJ - A Case Study for Meta-Level
Specifications, Proceedings of the 24th International Symposium on Logic-Based
Program Synthesis and Transformation (24th LOPSTR), LNCS 8981, Springer,
pp.182-198 (2014). https://doi.org/10.1007/978-3-319-17822-6_11
[67]
Kazuhiro Ogata, Thapana Chaimanont, Min Zhang: Formal Modeling and Analysis of Time-
and Resource-sensitive Simple Business Processes, 2nd International Symposium on
Dependable Computing and Internet of Things (2nd DCIT), IEEE, pp.1-10
(2015). https://doi.org/10.1109/DCIT.2015.23
[68]
Ha Thi Thu Doan, Wenjie
Zhang, Min Zhang, Kazuhiro Ogata: Model Checking Chandy-Lamport Distributed Snapshot Algorithm Revisited, 2nd
International Symposium on Dependable Computing and Internet of Things (2nd
DCIT), IEEE, pp.30-39 (2015). https://doi.org/10.1109/DCIT.2015.13
[69]
Hiroyuki Yoshida, Kokichi Futatsugi, Kazuhiro Ogata: Formalization and
Verification of Declarative Cloud Orchestration, 17th International Conference
on Formal Engineering Methods (17th ICFEM), LNCS 9407, Springer, pp.33-49
(2015). https://doi.org/10.1007/978-3-319-25423-4_3
[70]
Min Zhang, Kazuhiro Ogata, Kokichi Futatsugi: Towards a Formal Approach to Modeling and
Verifying the Design of Dynamic Software Updates, 22nd Asia-Pacific Software
Engineering Conference (22nd APSEC), IEEE, pp.159-166 (2015). https://doi.org/10.1109/APSEC.2015.28
[71]
Masaki
Nakamura, Daniel Gaina, Kazuhiro Ogata, Kokichi Futatsugi: Proving
Sufficient Completeness of Constructor-Based Algebraic Specifications, 7th
International Conference on Computer Science and its Applications (CSA-15) and
the International Conference on Ubiquitous Information Technologies and
Applications (CUTE 2015), LNEE 373, Springer, pp.15-21 (2015). https://doi.org/10.1007/978-981-10-0281-6_3
[72]
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, Late Breaking Papers of
the 25th International Conference on Inductive Logic Programming, CEUR Workshop
Proceedings 1636, CEUR-WS.org, pp.33--47 (2015). http://ceur-ws.org/Vol-1636/paper-03.pdf
[73] Adrián Riesco, Kazuhiro
Ogata, Kokichi Futatsugi: CafeInMaude: A CafeOBJ Interpreter in Maude. 19th International Conference
on Fundamental Approaches to Software Engineering (19th FASE), LNCS 9633,
Springer, pp.377-380 (2016). https://doi.org/10.1007/978-3-662-49665-7_22
[74]
Ha Thi Thu Doan, Francois Bonnet, Kazuhiro
Ogata: Model Checking of a Mobile Robots Perpetual Exploration Algorithm,
6th International Workshop on SOFL+MSVL (6th SOFL+MSVL), LNCS 10189, Springer,
pp.201-219 (2016). https://doi.org/10.1007/978-3-319-57708-1_12
[75]
Ha Thi Thu Doan, Francois Bonnet, Kazuhiro
Ogata: Specifying a Distributed Snapshot Algorithm as a Meta-program and
Model Checking it at Meta-level, 37th IEEE International Conference on
Distributed Computing Systems (37th ICDCS), IEEE, pp.1586-1596 (2017). https://doi.org/10.1109/ICDCS.2017.176
[76]
Adrián Riesco, Kazuhiro
Ogata: A Formal Proof Generator from Semi-formal Proof, 14th International
Colloquium on Theoretical Aspects of Computing (14th ICTAC), LNCS 10580,
Springer, pp.3-12 (2017). https://doi.org/10.1007/978-3-319-67729-3_1
[77]
Tam Thi Thanh Nguyen, Kazuhiro Ogata: A Way to
Comprehend Counterexamples Generated by the Maude LTL Model Checker, 7th Annual
Conference on Software Analysis, Testing and Evolution (SATE 2017), IEEE,
pp.53-62 (2017). https://doi.org/10.1109/SATE.2017.15
[78]
Tam Thi Thanh Nguyen, Kazuhiro Ogata: Graphical
Animations of State Machines, 15th IEEE International Conference on Dependable,
Autonomic and Secure Computing (15th DASC), IEEE, pp.604-611 (2017). https://doi.org/10.1109/DASC-PICom-DataCom-CyberSciTec.2017.107
[79]
Tam Thi Thanh Nguyen, Kazuhiro Ogata:
Graphically perceiving characteristics of the MCS lock and model checking them,
7th International Workshop on SOFL+MSVL (7th SOFL+MSVL), LNCS 10795, Springer,
pp.3-23 (2017). https://doi.org/10.1007/978-3-319-90104-6_1
[80]
Dorian Daudier, Trinh Ngoc Quoc Bao, Kazuhiro Ogata: A proof score approach to formal
verification of an imperative programming language compiler, 7th International
Workshop on SOFL+MSVL (7th SOFL+MSVL), LNCS 10795, Springer, pp.200-217
(2017). https://doi.org/10.1007/978-3-319-90104-6_13
[81]
Xuan-Linh Ha, Kazuhiro Ogata: Writing concurrent Java programs based on
CafeOBJ specifications, 24th Asia-Pacific Software
Engineering Conference (24th APSEC), IEEE, pp.618-623 (2017). https://doi.org/10.1109/APSEC.2017.75
[82]
Ha Thi Thu Doan, Francois Bonnet, Kazuhiro
Ogata: Model Checking of Robot Gathering, 21st International Conference on
Principles of Distributed Systems (21st OPODIS), LIPIcs, pp.12:1–12:16
(2017). https://doi.org/10.4230/LIPIcs.OPODIS.2017.12
[83]
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,
7th International Conference on Software and Computer
Applications (7th ICSCA),
ACM, pp.153-157 (2018). https://doi.org/10.1145/3185089.3185104
[84]
May Thu Aung, Tam Thi Thanh Nguyen, Kazuhiro
Ogata: Analysis of Two Flawed Versions of A Mutual Exclusion Protocol with
Maude and SMGA, 7th International Conference on Software and Computer
Applications (7th ICSCA), ACM, pp.194-198
(2018). https://doi.org/10.1145/3185089.3185110
[85]
Yati Phyo, Kazuhiro
Ogata: Analysis of Some Variants of the Anderson Array-Based Queuing Mutual
Exclusion Protocol with Model Checking and Graphical Animations, 5th
International Conference on Dependable Systems and Their Applications (5th DSA),
IEEE, pp.126-135 (2018). https://doi.org/10.1109/DSA.2018.00030
[86]
Shouki Sakamoto, Kazuhiro Ogata: Model Checking
of the Suzuki-Kasami Distributed Mutual Exclusion
Algorithm with SPIN, 5th International Conference on Dependable Systems and
Their Applications (5th DSA), IEEE, pp.136-141
(2018). https://doi.org/10.1109/DSA.2018.00031
[87]
Yati Phyo, Kazuhiro
Ogata: Formal
Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion
Protocol for Ad Hoc Mobile Networks, 25th Asia-Pacific Software Engineering
Conference (25th APSEC), IEEE, pp.89-98 (2018). https://doi.org/10.1109/APSEC.2018.00023
[88]
Jiaqi Qian, Min Zhang, Yi Wang, Kazuhiro Ogata:
KupC: A Formal Tool for Modeling and Verifying Dynamic
Updating of C Programs, 22nd International Conference on Fundamental Approaches
to Software Engineering (22nd FASE), LNCS 11424, Springer, pp.299-305
(2019). https://doi.org/10.1007/978-3-030-16722-6_17
[89]
Kazuhiro Ogata: Formal
Specification and Model Checking of A* Algorithm, 31st International Conference
on Software Engineering and Knowledge Engineering (31st SEKE), KSI Research
Inc., pp.181-186 (2019). https://doi.org/10.18293/SEKE2019-022
[90]
Moe Nandi Aung, Yati Phyo,
Kazuhiro Ogata: Formal
Specification and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control
Protocol, 31st International Conference on Software Engineering and Knowledge
Engineering (31st SEKE), KSI Research Inc., pp.159-164 (2019). https://doi.org/10.18293/SEKE2019-021
[91]
Canh Do Minh, Kazuhiro Ogata: Specification-based
Testing with Simulation Relations, 31st International Conference on Software
Engineering and Knowledge Engineering (31st SEKE), KSI Research Inc., pp.107-112
(2019). https://doi.org/10.18293/SEKE2019-027
[92]
Dang Duy Bui, Kazuhiro Ogata: Graphical
Animations of the Suzuki-Kasami Distributed Mutual
Exclusion Protocol,
25th International DMS Conference on Visualization and Visual Languages (25th
DMSVIVA), KSI Research Inc., pp.125-134 (2019). https://doi.org/10.18293/DMSVIVA2019-012
[93]
Ha Thi Thu Doan, Adrián
Riesco, Kazuhiro Ogata: An Environment for
Specifying and Model Checking Mobile Ring Robot Algorithms. 21st International
Symposium on Stabilization, Safety, and Security of Distributed Systems (21st
SSS), LNCS 11914, Springer, pp.111-126 (2019). https://doi.org/10.1007/978-3-030-34992-9_10
[94]
Yati Phyo, Canh Do Minh, Kazuhiro Ogata: Toward development of a
tool supporting a 2-layer divide & conquer approach to leads-to model
checking, 2019 International Conference on Advanced Information Technologies
(ICAIT), IEEE, pp.250-255 (2019). https://doi.org/10.1109/AITC.2019.8920978
[95]
Eiichi Muramoto, Kazuhiro Ogata, Yoichi Shinoda: Formal Specification and Model Checking of a
Ride-sharing System in Maude, 9th International Workshop on SOFL+MSVL (9th
SOFL+MSVL), LNCS 12028, Springer, pp.187-204 (2020). https://doi.org/10.1007/978-3-030-41418-4_14
[96]
Canh Do Minh, Kazuhiro Ogata: A Divide &
Conquer Approach to Testing Concurrent Java Programs with JPF and Maude, 9th
International Workshop on SOFL+MSVL (9th SOFL+MSVL), LNCS 12028, Springer,
pp.42-58
(2020). https://doi.org/10.1007/978-3-030-34992-9_10
[97]
Dang Duy Bui, Kazuhiro Ogata: Better
State Pictures Facilitating State Machine Characteristic Conjecture,
26th International DMS Conference on Visualization and Visual Languages (26th
DMSVIVA), KSI Research Inc., pp.7-12 (2020). https://doi.org/10.18293/DMSVIVA20-007
[98]
Duong Dinh Tran, Kazuhiro Ogata: Formal verification of an abstract
version of Anderson protocol with CafeOBJ, CiMPA and CiMPG, 32nd
International Conference on Software Engineering and Knowledge Engineering (32nd
SEKE), KSI Research Inc., pp.287-292 (2020). https://doi.org/10.18293/SEKE2020-064
[99]
Canh Do Minh, Kazuhiro Ogata: Parallel
stratified random testingfor concurrent programs, IEEE 20th International
Conference on Software Quality, Reliability and Security Companion (QRS-C),
IEEE, pp.79-86 (2020). https://doi.org/10.1109/QRS-C51114.2020.00024
[100]
Masaki Nakamura, Shuki Higashi, Kazutoshi Sakakibara, Kazuhiro Ogata:
Formal verification of Fischer's real-time mutual exclusion protocol by the
OTS/CafeOBJ method, 59th Annual Conference of the Society of Instrument and
Control Engineers of Japan (59th SICE), IEEE, pp.1210-1215 (2020). https://ieeexplore.ieee.org/document/9240272
[101]
Adrián Riesco, Kazuhiro
Ogata: CiMPG+F: A Proof Generator and Fixer-Upper for CafeOBJ
Specifications, 17th International Colloquium on Theoretical Aspects of
Computing (17th ICTAC), LNCS 12545, Springer, pp.64-82 (2020). https://doi.org/10.1007/978-3-030-64276-1_4
[102]
Canh Do Minh, Kazuhiro Ogata: A divide &
conquer approach to testing concurrent programs with JPF, 27th Asia-Pacific
Software Engineering Conference (27th APSEC), IEEE, pp.356-364 (2020). https://doi.org/10.1109/APSEC51365.2020.00044
[103]
Duong Dinh Tran, Dang Duy Bui, Parth
Gupta, Kazuhiro Ogata: Lemma Weakening for State Machine Invariant
Proofs, 27th Asia-Pacific Software Engineering Conference (27th APSEC), IEEE,
pp.21-30 (2020). https://doi.org/10.1109/APSEC51365.2020.00010
[104]
Masaki Nakamura, Kazutoshi Sakakibara, Yuki Okura, Kazuhiro Ogata: Formal
verification of multitask hybrid systems by the OTS/CafeOBJ method, 33rd
International Conference on Software Engineering and Knowledge Engineering (33rd
SEKE), KSI Research Inc., pp.114-119 (2021). https://doi.org/10.18293/SEKE2021-029
[105]
Thet Wai Mon, Shuho Fujii, Duong Dinh Tran, Kazuhiro Ogata: Formal
verification of IFF & NSLPK authentication protocols with CiMPG, 33rd
International Conference on Software Engineering and Knowledge Engineering (33rd
SEKE), KSI Research Inc., pp.120-125 (2021). https://doi.org/10.18293/SEKE2021-037
[106]
Naoki Asae, Duong Dinh Tran, Kazuhiro Ogata: Formal verification of
Anderson mutual exclusion protocol by introducing an auxiliary variable,
33rd International Conference on Software Engineering and Knowledge Engineering
(33rd SEKE), KSI Research Inc., pp.126-131 (2021). https://doi.org/10.18293/SEKE2021-038
[107]
Duong Dinh Tran, Kentaro Waki, Kazuhiro Ogata: Formal specification and
model checking of a recoverable wait-free version of MCS, 33rd International
Conference on Software Engineering and Knowledge Engineering (33rd SEKE), KSI
Research Inc., pp.138-143 (2021). https://doi.org/10.18293/SEKE2021-065
[108]
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, 27th International DMS Conference on Visualization and Visual
Languages (27th DMSVIVA), KSI Research Inc., pp.22-28 (2021). https://doi.org/10.18293/DMSVIVA2021-004
[109]
Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata: Graphical
Animations of the NSLPK Authentication Protocol, 27th International DMS
Conference on Visualization and Visual Languages (27th DMSVIVA), KSI Research
Inc., pp.29-35 (2021). https://doi.org/10.18293/DMSVIVA2021-005
[110]
Yati Phyo, Canh Minh Do, Kazuhiro Ogata: A support tool for the
L + 1-layer divide & conquer approach to leads-to model checking, 45th IEEE
Computer Society Computers, Software, and Applications Conference 45th
(COMPSAC), IEEE, pp.854-863 (2021). https://doi.org/10.1109/COMPSAC51774.2021.00118
[111]
Iakovos
Ouranos, Petros Stefaneas, Kazuhiro Ogata: Towards algebraic
specification and verification of airport baggage handling systems algorithms,
9th International Symposium on Symbolic Computation in Software Science (SCSS
2021), short and work-in-progress papers, Research Institute of Sympolic
Computation (RISC), Johannes Kepler University Linz (JKU), pp.34-39, (2021) https://doi.org/10.35011/risc.21-16
[112]
Yati Phyo, Canh Minh Do, Kazuhiro Ogata: A Divide & Conquer Approach
to Conditional Stable Model Checking, 18th International Colloquium on
Theoretical Aspects of Computing (ICTAC 2021), LNCS 12819, Springer, pp.105-111,
(2021) https://doi.org/10.1007/978-3-030-85315-0_7
[113]
Canh Minh Do, Yati Phyo, Adrián Riesco, Kazuhiro Ogata: A Parallel Stratified Model
Checking Technique/Tool for Leads-to Properties, 7th International Symposium on
System and Software Reliability (ISSSR), IEEE, pp.155-166, (2021) https://doi.org/10.1109/ISSSR53171.2021.00011
[114]
Minxuan Liu, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata: Formal
Specification and Model Checking of an Autonomous Vehicle Merging Protocol, IEEE
21st International Conference on Software Quality, Reliability and Security
Companion (QRS-C), IEEE, pp.333-342 (2021). https://doi.org/10.1109/QRS-C55045.2021.00057
[115]
Canh Minh Do, Adrián Riesco, Santiago Escobar and Kazuhiro Ogata:
Parallel Maude-NPA for Cryptographic Protocol Analysis, 14th International
Workshop on Rewriting Logic and its Applications (WRLA 2022), LNCS 13252,
Springer, pp.253-273, (2022). https://doi.org/10.1007/978-3-031-12441-9_13
[116] Duong Dinh Tran, Kazuhiro Ogata: IPSG: Invariant Proof Score
Generation, 5th International Workshop on Advances in Artificial Intelligence
and Machine Learning (AIML 2022): Towards Trustworthy AI, IEEE, pp.1050-1055
(2022) https://doi.org1/0.1109/COMPSAC54236.2022.00164
[117]
Canh Minh Do, Yati Phyo, Kazuhiro Ogata: A divide & conquer approach
to until and until stable model checking, 34th International Conference on
Software Engineering & Knowledge Engineering (SEKE 2022), KSI Research Inc.,
pp.388-393, (2022) https://doi.org/10.18293/SEKE2022-058
[118]
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, 34th International Conference on Software
Engineering & Knowledge Engineering (SEKE 2022), KSI Research Inc.,
pp.382-387, (2022) https://doi.org/10.18293/SEKE2022-097
[119]
Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata, Adrian Riesco: Integration
of SMGA and Maude to Facilitate Characteristic Conjecture, 28th International
DMS Conference on Visualization and Visual Languages (DMSVIVA 2022), KSI
Research Inc., pp.45-54, (2022) https://doi.org/10.18293/DMSVIVA22-006
[120]
Dang Duy Bui, Minxuan Liu, Kazuhiro Ogata: Graphical Animations of an
Autonomous Vehicle Merging Protocol, 28th International DMS Conference on
Visualization and Visual Languages (DMSVIVA 2022), KSI Research Inc., pp.16-22,
(2022) https://doi.org/10.18293/DMSVIVA22-009
[121]
Moe Nandi Aung, Yati Phyo, Canh Minh Do, and Kazuhiro Ogata: A Tool for
Model Checking Eventual Model Checking in a Stratified Way, International
Conference on Dependable Systems and Their Applications (DSA 2022), IEEE,
pp.270-279, (2022) https://doi.org/10.1109/DSA56465.2022.00045
[122]
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub
Otmani: Formal specification and model checking of lattice-based key
encapsulation mechanisms in Maude, International Workshop on Formal Analysis and
Verification of Post-Quantum Cryptographic Protocols 2022 (FAVQC 2022), CEUR
Workshop Proceedings 3280, CEUR-WS.org, pp.16--31 (2022). https://ceur-ws.org/Vol-3280/paper2.pdf
[123]
Víctor García, Santiago Escobar, Kazuhiro Ogata: Modeling and
verification of the post-quantum key encapsulation mechanism KYBER using Maude,
International Workshop on Formal Analysis and Verification of Post-Quantum
Cryptographic Protocols 2022 (FAVQC 2022), CEUR Workshop Proceedings 3280,
CEUR-WS.org, pp.32--49 (2022). https://ceur-ws.org/Vol-3280/paper3.pdf
[124]
Duong Dinh Tran, Canh Minh Do, Santiago Escobar and Kazuhiro Ogata:
Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security
analysis, International Workshop on Formal Analysis and Verification of
Post-Quantum Cryptographic Protocols 2022 (FAVQC 2022), CEUR Workshop
Proceedings 3280, CEUR-WS.org, pp.50--64 (2022). https://ceur-ws.org/Vol-3280/paper4.pdf
[125]
Takanori Ishibashi, Kazuhiro Ogata: Formal Specification and Model
Checking of Raft Leader Election in Maude, 12th International Conference on
Software and Computer Applications (12th ICSCA),
ACM, pp.41-45 (2023). https://doi.org/10.1145/3587828.3587835
[126]
Naomi Okumura, Kazuhiro Ogata: A way to find counterexamples located at
deep positions with domain knowledge of authentication protocols, 12th
International Conference on Software and Computer Applications (12th ICSCA),
ACM, pp.206-211 (2023) https://doi.org/10.1145/3587828.3587859.
[127] Canh Minh Do, Kazuhiro Ogata: Symbolic Model Checking Quantum
Circuits in Maude, 35th International Conference on Software Engineering &
Knowledge Engineering (SEKE 2023), KSI Research Inc., pp.103-108, (2023) https://doi.org/10.18293/SEKE2023-014
[128]
Takanori Ishibashi, Kazuhiro Ogata: Formal Specification and Model
Checking of Raft Log Replication in Maude, 29th International DMS Conference on
Visualization and Visual Languages (DMSVIVA 2023), KSI Research Inc., pp.1-6,
(2023) https://doi.org/10.18293/DMSVIVA23-010
[招待講演(国際会議等)]
[1]
Kazuhiro Ogata: Analysis of Alternating Bit Protocol 1 & 2, Sinaia
School on Formal Verification of Software Systems, Sinaia, Romania, 3-10 March
2008 http://www.jaist.ac.jp/~kokichi/class/SinaiaSchoolFVSS0803/
[2]
Kazuhiro Ogata: Analysis of Simple Communication Protocol 1 & 2,
Sinaia School on Formal Verification of Software Systems, Sinaia, Romania, 3-10
March 2008 http://www.jaist.ac.jp/~kokichi/class/SinaiaSchoolFVSS0803/
[3]
Kazuhito Ogata: Proof Score Writing for QLOCK in OTS/CafeOBJ, JAIST
Advanced School on Formal Specification and Systems Verification 2010
(JAIST-FSSV2010), JAIST, Nomi, Ishikawa, Japan and Kanazawa Excel Hotel Tokyu,
Kanazawa, Ishikawa, Japan, March 1st-5th, 2010 http://www.jaist.ac.jp/~ogata/ldl/jaist-fssv2010/lectureMaterials/index.html
[4]
Kazuhiro Ogata: Specification of NSLPK, JAIST Advanced School on Formal
Specification and Systems Verification 2010 (JAIST-FSSV2010), JAIST, Nomi,
Ishikawa, Japan and Kanazawa Excel Hotel Tokyu, Kanazawa, Ishikawa, Japan, March
1st-5th, 2010 http://www.jaist.ac.jp/~ogata/ldl/jaist-fssv2010/lectureMaterials/index.html
[5]
Kazuhiro Ogata: Verification of NSLPK, JAIST Advanced School on Formal
Specification and Systems Verification 2010 (JAIST-FSSV2010), JAIST, Nomi,
Ishikawa, Japan and Kanazawa Excel Hotel Tokyu, Kanazawa, Ishikawa, Japan, March
1st-5th, 2010 http://www.jaist.ac.jp/~ogata/ldl/jaist-fssv2010/lectureMaterials/index.html
[6]
Kazuhiro Ogata: A Collaborative Use of CafeOBJ and Maude, JAIST Advanced
School on Formal Specification and Systems Verification 2010 (JAIST-FSSV2010),
JAIST, Nomi, Ishikawa, Japan and Kanazawa Excel Hotel Tokyu, Kanazawa, Ishikawa,
Japan, March 1st-5th, 2010 http://www.jaist.ac.jp/~ogata/ldl/jaist-fssv2010/lectureMaterials/index.html
[7] Kazuhiro
Ogata: Model checking designs with CafeOBJ - A contrast with a software
model checker, Workshop on Formal Method and Internet of Mobile Things (FMIMT),
East China Normal University (ECNU), Shanghai, Nov. 27th-28th, 2014 https://sei.ecnu.edu.cn/Data/View/596
[8]
Kazuhiro Ogata: Proof Script Generation from Proof Scores, The 2019 Joint
Workshop on Formal Methods, East China Normal University (ECNU), Shanghai,
China, December 12-13, 2019 https://zhmtechie.github.io/
[9]
Kazuhiro Ogata: Proof Script Generation from Proof Scores, SCIENCE AND
TECHNOLOGY AUTUMN CAMP (ST-Camp 2019) ARTIFICIAL INTELLIGENCE: FUNDAMENTAL &
APPLICATION, Danang, Vietnam, Oct 21-23, 2019
[10] Kazuhiro Ogata: A
stratified way to mitigate the state space explosion in model checking, The 12th
IEEE International Conference on KNOWLEDGE AND SYSTEMS ENGINEERING (KSE 2020),
Can Tho, Vietnam, November 12 - 14, 2020. https://kse-conference.org/
[11]
Kazuhiro Ogata: Model checking based on algebraic specifications and some
advanced topics, International Workshop on Frontiers of Software Reliability
Engineering, Online, December 1-3, 2022. http://www.wut-dscl.cn/workshops/workshop.html
[招待講演(国内会議等)]
[1]
緒方和博：代数仕様言語・処理系のシステム検証への応用、ソフトウェアシンポジウム2009，ソフトウェア技術者協会、札幌、２００９年６月１７日（水）〜１９日（金）https://www.sec.jp/post/view/id/6129
[2]
緒方和博：CafeOBJによるシステム検証、第165回ソフトウェア工学研究発表会、情報処理学会、JAIST、2009年7月2日(木)〜3日(金)
http://www.ipsj.or.jp/09sig/kaikoku/2009/SE165.html
[3]
緒方和博：不変性モデル検査器としてのCafeOBJ、2012年ソサイエティ大会、MSS(システム数理と応用研究会)企画「システム数理における様々なツールの紹介」、電子情報通信学会、富山大学、2012年9月11日(火)〜14日(金)
https://www.ieice.org/es/jpn/internal/
[1] 五百蔵重典，緒方和博，二木厚吉：項の構造を考慮したAC照合，第3回ソフトウェア工学の基礎ワークショップ(第3回FOSE)，pp.106-109
(1996)．
[2] 五百蔵重典，緒方和博，二木厚吉：CafeOBJのモジュールシステムの設計およびCafeOBJによる検証，第5回ソフトウェア工学の基礎ワークショップ(第5回FOSE)，pp.209-218
(1998)．
[3] 清野貴博，緒方和博，二木厚吉：代数仕様言語CafeOBJによる鉄道信号システムの記述と検証，第6回ソフトウェア工学の基礎ワークショップ(第6回FOSE)，pp.180-187 (1999)．
[4] 清野貴博，緒方和博，二木厚吉，日比野靖：実時間制約を考慮したマルチタスキングのモデル化，第8回ソフトウェア工学の基礎ワークショップ(第8回FOSE)，pp.143-146 (2001)．
[5] 清野貴博，緒方和博，二木厚吉：項書換えを用いた安全性検証の組織化，第9回ソフトウェア工学の基礎ワークショップ(第9回FOSE)，pp.107-118 (2002)．
[6] 中野昌弘, 中村正樹,
緒方和博, 二木厚吉：SMVによるOTS/CafeOBJ仕様のモデル検査，第11回ソフトウェア工学の基礎ワークショップ(第11回FOSE)，pp.129- 140
(2004)．
[7] 清野貴博，加藤淳，緒方和博，二木厚吉：書き換えによるOtway-Rees認証プロトコルの検証，第11回ソフトウェア工学の基礎ワークショップ(第11回FOSE)，pp.153-156
(2004)．
[国内論文誌チュートリアル(全文査読有)]
[1] 二木厚吉，緒方和博，中村正樹： CafeOBJ入門(1) - 形式手法とCafeOBJ，コンピュータソフトウェア(日本ソフトウェア科学会論文誌)，25(2)：1-13，2008．
[2] 中村正樹，二木厚吉，緒方和博：CafeOBJ 入門(2) - 構文と意味，コンピュータソフトウェア(日本ソフトウェア科学会論文誌)，25(2)：14-27，2008．
[3] 中村正樹，二木厚吉，緒方和博：CafeOBJ 入門(3) - 等式推論と項書換システム，コンピュータソフトウェア(日本ソフトウェア科学会論文誌)，25(3)：69-80，2008．
[4]
二木厚吉，緒方和博，中村正樹： CafeOBJ入門(4) - 証明譜による検証法，コンピュータソフトウェア(日本ソフトウェア科学会論文誌)，25(4)：68-84，2008．
[5] 緒方和博，二木厚吉，中村正樹： CafeOBJ入門(5) - 認証プロトコルの検証，コンピュータソフトウェア(日本ソフトウェア科学会論文誌)，26(1)：71-83，2009．
[6]
緒方和博，二木厚吉，中村正樹： CafeOBJ入門(6) - 通信プロトコルの検証，コンピュータソフトウェア(日本ソフトウェア科学会論文誌)，26(2)：93-106，2009．
[国内論文誌解説(全文査読有)]
[1] 緒方和博，中村正樹，二木厚吉：Maude：書換え論理に基づく計算機言語および処理系，コンピュータソフトウェア(日本ソフトウェア科学会論文誌)，25(2)：78-84，2008．
[2]
緒方和博：代数仕様に基づく実時間システムの検証，計測と制御，48(11)：816-821，2009．
[著書・編書]
[1] 緒方和博，中村正樹，二木厚吉：代数仕様，電子情報通信学会「知識ベース」，7群（コンピュータ・ソフトウェア）
– 1編（ソフトウェア基礎） – 1章（計算モデル）：34-39，2010．
[2] Kazuhiro Ogata: Special Section on Formal
Approach, IEICE TRANSACTIONS on Information and Systems, E96-D(6), IEICE, 2013.
[3] Shusaku
Iida, Jose Meseguer, and Kazuhiro Ogata (Eds): Specification, Algebra, and Software: Essays Dedicated
to Kokichi Futatsugi,
Lecture Notes in Computer Science (LNCS), Volume 8373, Springer, ISSN 0302-9743,
2014. https://doi.org/10.1007/978-3-642-54624-2
[4]
Kazuhiro Ogata, Mark Lawford, Shaoying Liu (Eds): 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 https://doi.org/10.1007/978-3-319-47846-3
[5]
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. https://ceur-ws.org/Vol-3280/
[6]
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) https://doi.org/10.1016/j.scico.2022.102912