業績リスト

[国際論文誌論文(全文査読有)]

[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.
[2] Kazuhiro Ogata and Kokichi Futatsugi: Flaw and modification of the iKP electronic payment protocols, Information Processing Letters, 86(2): 57-62, Elsevier, 2003.
[3] Razvan Diaconescu, Kokichi Futatsugi and Kazuhiro Ogata: CafeOBJ: Logical Foundation and Methodologies, Computing and Informatics, 22(3): 257-283, Slovak Academic Press, 2003.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[18] Kokichi Futatsugi, Daniel Gaina and Kazuhiro Ogata: Principles of proof scores in CafeOBJ, Theoretical Computer Science (TCS), 464: 90-112, Elsevier, 2012.
[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.
[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.
[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. 
[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.
[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.
[24] Adrian Riesco, Kazuhiro Ogata, Futatsugi Kokishi: A Maude Environment for CafeOBJ, Formal Aspects of Computing, Springer (FAoC), 2016 (to appear).

[国際会議・シンポジウム・ワークショップ論文(全文査読有)]

[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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).
[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)
[72] 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).
[73] Ha Thi Thu Doan, Francois Bonnet, Kazuhiro Ogata: Model Checking of a Mobile Robots Perpetual Exploration Algorithm, 7th International Workshop on SOFL+MSVL (7th SOFL+MSVL), LNCS, Springer, to appear.


[国内論文誌論文(全文査読有)]

[1] 緒方和博,栗原聡,稲荷幹夫,土居範久:MultithreadSmalltalk,コンピュータソフトウェア(日本ソフトウェア科学会論文誌)11(4):69-861994
[2] 緒方和博,土居範久:MultithreadSmalltalkのオブジェクト割付けの改善:複数プロセスでのオブジェクト割付けの効率化,コンピュータソフトウェア(日本ソフトウェア科学会論文誌)14(6):3-141997
[3] 五百蔵重典,緒方和博,二木厚吉:項書換え抽象機械TRAMの設計と実装,電子情報通信学会論文誌 D-IJ83-D-I(2):255-2632000
[4] 緒方和博,二木厚吉:書き換えによるセキュリティプロトコルの帰納的検証,コンピュータソフトウェア(日本ソフトウェア科学会論文誌)20(3):54-722003
[5] 清野貴博,緒方和博,二木厚吉:項書換えを用いた安全性検証の組織化,コンピュータソフトウェア(日本ソフトウェア科学会論文誌)20(5):32-452003
[6] 中村正樹, 緒方和博, 二木厚吉:項書き換えシステムにおける可簡約演算子とその応用,情報処理学会論文誌:プログラミング,46 (SIG 6; PRO25):47-592005
[7] Jianwen Xiang, Kazuhiro Ogata, Weiqiang Kong and Kokichi Futatsugi: From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ, コンピュータソフトウェア(日本ソフトウェア科学会論文誌)23(3):134-1462006.

[国内会議・シンポジウム・ワークショップ論文(全文査読有)]

[1] 五百蔵重典,緒方和博,二木厚吉:項の構造を考慮したAC照合,第3回ソフトウェア工学の基礎ワークショップ(3FOSE)pp.106-109 (1996)
[2] 五百蔵重典,緒方和博,二木厚吉:CafeOBJのモジュールシステムの設計およびCafeOBJによる検証,第5回ソフトウェア工学の基礎ワークショップ(5FOSE)pp.209-218 (1998)
[3] 清野貴博,緒方和博,二木厚吉:代数仕様言語CafeOBJによる鉄道信号システムの記述と検証,第6回ソフトウェア工学の基礎ワークショップ(6FOSE)pp.180-187 (1999)
[4] 清野貴博,緒方和博,二木厚吉,日比野靖:実時間制約を考慮したマルチタスキングのモデル化,第8回ソフトウェア工学の基礎ワークショップ(8FOSE)pp.143-146 (2001)
[5] 清野貴博,緒方和博,二木厚吉:項書換えを用いた安全性検証の組織化,第9回ソフトウェア工学の基礎ワークショップ(9FOSE)pp.107-118 (2002)
[6] 中野昌弘, 中村正樹, 緒方和博, 二木厚吉:SMVによるOTS/CafeOBJ仕様のモデル検査,第11回ソフトウェア工学の基礎ワークショップ(11FOSE)pp.129- 140 (2004)
[7] 清野貴博,加藤淳,緒方和博,二木厚吉:書き換えによるOtway-Rees認証プロトコルの検証,第11回ソフトウェア工学の基礎ワークショップ(11FOSE)pp.153-156 (2004)

[国内論文誌チュートリアル(全文査読有)]

[1] 二木厚吉,緒方和博,中村正樹: CafeOBJ入門(1) - 形式手法とCafeOBJ,コンピュータソフトウェア(日本ソフトウェア科学会論文誌)25(2)1-132008
[2] 中村正樹,二木厚吉,緒方和博CafeOBJ 入門(2) - 構文と意味,コンピュータソフトウェア(日本ソフトウェア科学会論文誌)25(2)14-272008
[3] 中村正樹,二木厚吉,緒方和博CafeOBJ 入門(3) - 等式推論と項書換システム,コンピュータソフトウェア(日本ソフトウェア科学会論文誌)25(3)69-802008
[4] 二木厚吉,緒方和博,中村正樹: CafeOBJ入門(4) - 証明譜による検証法,コンピュータソフトウェア(日本ソフトウェア科学会論文誌)25(4)68-842008
[5] 緒方和博,二木厚吉,中村正樹: CafeOBJ入門(5) - 認証プロトコルの検証,コンピュータソフトウェア(日本ソフトウェア科学会論文誌)26(1)71-832009
[6] 緒方和博,二木厚吉,中村正樹: CafeOBJ入門(6) - 通信プロトコルの検証,コンピュータソフトウェア(日本ソフトウェア科学会論文誌)26(2)93-1062009

[国内論文誌解説(全文査読有)]

[1] 緒方和博,中村正樹,二木厚吉:Maude:書換え論理に基づく計算機言語および処理系,コンピュータソフトウェア(日本ソフトウェア科学会論文誌)25(2)78-842008
[2] 緒方和博:代数仕様に基づく実時間システムの検証,計測と制御,48(11)816-8212009

[著書・編書]

[1] 緒方和博,中村正樹,二木厚吉:代数仕様,電子情報通信学会「知識ベース」,7群(コンピュータ・ソフトウェア) – 1編(ソフトウェア基礎) – 1章(計算モデル):34-392010
[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. .
[3] 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


Feb 13, 2017 by ogata