論文

• Takashi Tomita, Atsushi Ueno, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki.. Safraless LTL synthesis considering maximal realizability, Acta Informatica, pp. 1-38, Oct. 2016.
• Sohei Ito, Shigeki Hagihara, Naoki Yonezaki. Formulation of Homeostasis by Realisability on Linear Temporal Logic, Biomedical Engineering Systems and Technologies,, Communications in Computer and Information Science, Vol. 511, pp. 149-164, Jan. 2016.
• Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Qualitative analysis of gene regulatory networks by temporal logic, Theoretical Computer Science, Vol. 594, pp. 151-179, Aug. 2015.
• 冨田尭, 萩原茂樹, 伊藤宗平, 米崎直樹. 確率頻度時間論理の統計的モデル検査, コンピューターソフトウェア, 岩波書店, Vol. 31, No. 3, pp. 336-356, Aug. 2014.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Bounded Strong Satisfiability Checking of Reactive System Specifications, IEICE Transactions on Information and Systems, A Publication of the Information and Systems Society, Vol. E97-D, No. 7, pp. 1746-1755, July 2014.
• 冨田尭, 萩原茂樹, 米崎直樹. 平均利得時間論理とそれを用いた検証・最適化手法, コンピューターソフトウェア, 岩波書店, Vol. 31, No. 2, pp. 93-117, Apr. 2014.
• 安藤崇央, 萩原茂樹, 米崎直樹. SAT solverを用いるLTLタブロー構成法とその評価, 情報処理学会論文誌, Vol. 55, No. 2, pp. 909-921, Feb. 2014.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Complexity of Strong Satisfiability Problems for Reactive System Specifications, IEICE Transactions on Information and Systems, A Publication of the Information and Systems Society, Vol. E96-D, No. 10, pp. 2187-2193, Oct. 2013.
• Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Modular analysis of gene networks by linear temporal logic, Journal of Integrative Bioinformatics, Vol. 10, No. 2, 216, 2013.  公式リンク  
  
• Shigeki Hagihara, Hiroaki Oguro, Naoki Yonezaki. Kripke semantics for Epistemic Logic of Relational Information between Ciphertexts, Philippine Computing Journal, Vol. 7, No. 2, pp. 23-32, Dec. 2012.
• 安藤崇央, 宮本佑樹, 萩原茂樹, 米崎直樹. リアクティブシステム仕様に対する段階的充足可能性判定器の分散オブジェクト技術を利用した実装, コンピューターソフトウェア, 岩波書店, Vol. 28, No. 4, pp. 262-281, Nov. 2011.
• 萩原茂樹, 北村佑介, 島川昌也, 関戸聡, 米崎直樹. リアクティブシステム仕様を実現可能にするための環境制約の抽出, コンピューターソフトウェア, 岩波書店, Vol. 28, No. 3, pp. 132-146, Aug. 2011.
• 伊藤宗平, 萩原茂樹, 米崎直樹. プログラム依存グラフの操作的意味, コンピュータソフトウェア, Vol. 26, No. 3, pp. 109-135, Aug. 2009.
• 小黒博昭, 萩原茂樹, 米崎直樹. 記号論的暗号解析を用いたOblivious Transferプロトコルの解析, 電子情報通信学会論文誌 D, Vol. J92-D, No. 5, pp. 596-607, May 2009.
• 萩原茂樹, 友石正彦, 米崎直樹. 有限フレームを意味的基礎として持つ様相論理に対する分解証明法, コンピュータソフトウェア, Vol. 18, No. 0, pp. 78-91, Dec. 2000.

著書

• 萩原茂樹. 論理的検証法, 応用数理ハンドブック, 朝倉書店, pp. 238-239, Oct. 2013.
• 萩原茂樹, 米崎直樹. AbadiとRogawayによるメッセージの識別不可能性の形式化, 数理的技法による情報セキュリティ(シリーズ応用数理), 共立出版, Vol. 1, pp. 137-152, July 2010.

国際会議発表 (査読有り)

• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Efficiency of the Strong Satisfiability Checking Procedure for Reactive System Specifications, International Conference on Computer, Electronic Engineering and Information Science (CEEIS 2017), Dec. 2017.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Towards Improvements of Bounded Realizability Checking, Workshop on Computation: Theory and Practice (WCTP2017), Sept. 2017.
• Shigeki Hagihara, Masaya Shimakawa, Naoki Yonezaki. Discussion on Verification of Voting Protocols, 17th Philippine Computing Science Congress (PCSC 2017), Proceedings of the 17th Philippine Computing Science Congress, Mar. 2017.
• Shigeki Hagihara, Masahiko Tomoishi, Masaya Shimakawa, Naoki Yonezaki. Combining Unification and Rewriting in Proofs for Modal Logics with First-order Undefinable Frames, 5th International Conference on Computer Science, Electronics Technology and Automation (ICCSETA 2017), Preproceedings of 5th International Conference on Computer Science, Electronics Technology and Automation (ICCSETA 2017), Mar. 2017.
• Shigeki Hagihara, Yoshiharu Fushihara, Masaya Shimakawa, Masahiko Tomoishi, Naoki Yonezaki. Web server access trend analysis based on the Poisson distribution, 6th International Conference on Software and Computer Applications (ICSCA 2017), Preproceedings of 6th International Conference on Software and Computer Applications (ICSCA 2017), Feb. 2017.
• Masaya Shimakawa, Kenji Osari, Shigeki Hagihara, Naoki Yonezaki. Modularization of formal specifications for efficient synthesis of reactive systems, 6th International Conference on Software and Computer Applications (ICSCA 2017), Preproceedings of 6th International Conference on Software and Computer Applications (ICSCA 2017), Feb. 2017.
• Masaya Shimakawa, Yuuji Iwasaki, Shigeki Hagihara, Naoki Yonezaki. Discussion of LTL Subsets for Efficient Verification, Workshop on Computation: Theory and Practice (WCTP2016), Preproceedings of Workshop on Computation: Theory and Practice (WCTP2016), pp. 1-14, Sept. 2016.
• Shigeki Hagihara, Atsushi Ueno, Takashi Tomita, Masaya Shimakawa, Naoki Yonezaki. Simple synthesis of reactive systems with tolerance for unexpected environmental behavior, the 4th FME Workshop on Formal Methods in Software Engineering (FormaliSE '16), Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering (FormaliSE '16), ACM New York, pp. 15-21, May 2016.
• Shigeki Hagihara, Naoto Sato, Naoki Yonezaki. Toward Applicable Synthesis of Security Protocols for Data Transmission, 16h Philippine Computing Science Congress (PCSC 2016), Proceedings of the 16th Philippine Computing Science Congress, Mar. 2016.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki.. Towards Unbounded Realizability Checking, Workshop on Computation: Theory and Practice (WCTP2015), Preproceedings of Workshop on Computation: Theory and Practice (WCTP2015), pp. 80-90, Sept. 2015.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki.. Reducing Bounded Realizability Analysis to Reachability Checking, 9th International Workshop on Reachability Problems(RP 2015), Reachability Problems, Lecture Notes in Computer Science, Springer, Vol. 9328, pp. 140-152, Sept. 2015.
• Yoshiharu Fushihara, Shigeki Hagihara, Masahiko Tomoishi, Naoki Yonezaki. A new approach to analysis of access tendency of web server using Poisson distribution, 15h Philippine Computing Science Congress (PCSC 2015), Proceedings of the 15th Philippine Computing Science Congress, pp. 14-19, Mar. 2015.
• Sohei Ito, Shigeki Hagihara, Naoki Yonezaki. Approximate Analysis of Homeostasis of Gene Networks by Linear Temporal Logic using Network Motifs, 6th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS2015), proceedings of 5th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS2014), pp. 93-101, Jan. 2015.
• Shohei Mochizuki, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Fast Translation from LTL to Büchi Automata via Non-transition-based Automata, 16th International Conference on Formal Engineering Methods (ICFEM 2014), Formal Methods and Software Engineering, 16th International Conference on Formal Engineering Methods, ICFEM 2014, Lecture Notes in Computer Science, Springer, Vol. 8829, pp. 364-379, Nov. 2014.
• Kenji Osari, Shigeki Hagihara, Naoki Yonezaki. Discussion on modularization of specifications for efficient synthesis of reactive systems, 7th Symposium on Mathematical Aspects of Computer Science, SMACS2014, 7th Symposium on Mathematical Aspects of Computer Science, SMACS2014, Preproceedings, pp. 27-32, Nov. 2014.
• Takashi Tomita, Takahito Kimura, Shigeki Hagihara, Naoki Yonezaki. An Efficient Implementation of Satisfiability Checking for LTL with Mean-Payoff Constraints, Workshop on Computation: Theory and Practice (WCTP2014), Preproceedings of Workshop on Computation: Theory and Practice (WCTP2014), pp. 30-42, Oct. 2014.
• Shigeki Hagihara, Naoki Egawa, Masaya Shimakawa, Naoki Yonezaki. Minimal strongly unsatisfiable subsets of reactive system specifications, the 29th ACM/IEEE international conference on Automated software engineering (ASE2014), Proceedings of the 29th ACM/IEEE international conference on Automated software engineering (ASE2014), ACM New York, pp. 629-634, Sept. 2014.
• Shigeki Hagihara, Masahiko Tomoishi, Naoki Yonezaki. On Constructing Unification-based Proof Methods for Modal Logics with First-order Undefinable Frames, 14th Philippine Computing Science Congress (PCSC 2014), Proceedings of the 14th Philippine Computing Science Congress, pp. 22-27, Mar. 2014.
• Sohei Ito, Shigeki Hagihara, Naoki Yonezaki. A Qualitative Framework for Analysing homeostasis in Gene Networks, 5th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS2014), proceedings of 5th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS2014), pp. 5-16, Mar. 2014.
• Kenji Osari, Takuya Murooka, Kiyotaka Hagiwara, Takahiro Ando, Masaya Shimakawa, Sohei Ito, Shigeki Hagihara, Naoki Yonezaki. An object-oriented language for parameterised reactive system specification based on linear temporal logic, Workshop on Computation: Theory and Practice (WCTP2013), Preproceedings of Workshop on Computation: Theory and Practice (WCTP2013), pp. 94-113, Sept. 2013.
• Takashi Tomita, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. A Formal Ontology of Interactions with Intensional Quantitative Semantics, Workshop on Computation: Theory and Practice (WCTP-2012), Theory and Practice of Computation, Proceedings in Information and Communications Technology, Vol. 7, pp. 13-33, June 2013.
• Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Modular analysis of gene networks by linear temporal logic, proceedings of 9th International Symposium on Integrative Bioinformatics, pp. 43-54, Mar. 2013.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. SAT–Based Bounded Strong Satisfiability Checking of Reactive System Specifications, Information & Communication Technology - EurAsia Conference 2013 (ICT-EurAsia 2013), Information and Communicatiaon Technology, Lecture Notes in Computer Science, Vol. 7804, pp. 60-70, Mar. 2013.
• Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Qualitative analysis of gene regulatory networks using network motifs, proceedings of 4th International Conference on Bioinformatics Models, Methods and Algorithms (BIOINFORMATICS2013), pp. 15-24, Feb. 2013.
• Takashi Tomita, Shin Hiura, Shigeki Hagihara, Naoki Yonezaki. A Temporal Logic with Mean-Payoff Constraints, 14th International Conference on Formal Engineering Methods (ICFEM 2012), Formal Methods and Software Engineering, 14th International Conference on Formal Engineering Methods, ICFEM 2012, Lecture Notes in Computer Science, Springer, Vol. 7635, pp. 249-265, Nov. 2012.
• Sohei Ito, Takuma Ichinose, Masaya Shimakawa, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Modular analysis of gene networks using temporal logic (abstract), 5th Annual RECOMB Conference on Regulatory and Systems Genomics, with DREAM Challenges, program booklet, pp. 118-119, Nov. 2012.
• Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki. Complexity of Checking Strong Satisfiability of Reactive System Specifications, International Conference on Advances in Information Technology and Communication, AIT 2012, International Conference on Advances in Information Technology and Communication, AIT 2012, pp. 42-51, Sept. 2012.
• Shigeki Hagihara, Takahiro Arai, Masaya Shimakawa, Naoki Yonezaki. Developing Embedded Systems from Formal Specifications Written in Temporal Logic, the Third International Conference on Trends in Information, Telecommunication and Computing (ITC2012), Proceedings of the Third International Conference on Trends in Information, Telecommunication and Computing, Lecture Notes in Electrical Engineering, Springer, Vol. 150, pp. 107-113, Aug. 2012.
• Shigeki Hagihara, Hiroaki Oguro, Naoki Yonezaki. Completeness of a Deduction System for Relational Information between Ciphertexts based on Probabilistic Computational Semantics, Workshop on Computation: Theory and Practice (WCTP-2011), Theory and Practice of Computation, Proceedings in Information and Communications Technology, Springer, Vol. 5, pp. 116-132, May 2012.
• Takashi Tomita, Shigeki Hagihara, Naoki Yonezaki. Probabilistic Temporal Logic with Frequency Operators and Its Model Checking, 13th International Workshop on Verification of Infinite-State Systems (INFINITY 2011), Proceedings 13th International Workshop on Verification of Infinite-State Systems. 2011, Electronic Proceedings in Theoretical Computer Science, Vol. 73, pp. 79–93, Oct. 2011.
• Takahiro Shinozaki, Masakazu Sekijima, Shigeki Hagihara, Sadaoki Furui. Compact speech decoder based on pure functional programming, APSIPA ASC 2011, Proc. APSIPA ASC 2011, Oct. 2011.
• Sohei Ito, Takuma Ichinose, Naoko Izumi, Shigeki Hagihara, NAOKI YONEZAKI. Qualitative analysis of gene regulatory networks by approximation using network motifs, International Symposium on Integrative Bioinformatics 2011, Mar. 2011.
• Takashi Tomita, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Qualitative Inference Rules for Analysis of Biological Object Interactions, 9th International Conference on Bioinformatics, 9th International Conference on Bioinformatics, Abstracts, pp. 48, Sept. 2010.
• Sohei Ito, Naoko Izumi, Shigeki Hagihara, NAOKI YONEZAKI. Possible behavior analysis of Gene Regulatory Networks by Linear Temporal Logic, 9th International Conference on Bioinformatics, 9th International Conference on Bioinformatics, Abstracts, pp. 50, Sept. 2010.
• Sohei Ito, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Qualitative analysis of gene regulatory networks by satisfiability checking of Linear Temporal Logic, Proceedings of the 10th IEEE International Conference on Bioinformatics & Bioengineering, pp. 232-237, May 2010.
• Shigeki Hagihara, Yusuke Kitamura, Masaya Shimakawa, Naoki Yonezaki. Extracting Environmental Constraints to Make Reactive System Specifications Realizable, Proceedings of 16th Asia-Pacific Software Engineering Conference APSEC 2009, pp. 61-68, Dec. 2009.
• Sohei Ito, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. Analysis of gene regulatory networks by checking satisfiability of Linear Temporal Logic, CBI-KSBSB Joint Conference, CBI-KSBSB Joint Conference, P12-143, pp. 216, Nov. 2009.
• Takashi Tomita, Naoko Izumi, Shigeki Hagihara, Naoki Yonezaki. 2-layered Formal Interaction Ontology among Biological Processes with Quantitative Semantics, CBI-KSBSB Joint Conference, CBI-KSBSB Joint Conference, P12-144, pp. 217, Nov. 2009.
• Souhei Ito, Shigeki Hagihara, Naoki Yonezaki. An Operational Semantics of Program Dependence Graphs for Unstructured Programs, 11th Annual Asian Computing Science Conference (ASIAN 2006), Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, Lecture Notes in Computer Science, Springer Berlin, Vol. 4435, pp. 264-271, Jan. 2008.
• Sohei Ito, Shigeki Hagihara, Naoki Yonezaki. A Formal Ontology for Business Process Model TAP: Tasks-Agents-Products, Information Modeling and Knowledge Bases XIX, IOS Press, Vol. 166, pp. 290-297, 2008.
• Souhei Ito, Shigeki Hagihara, Naoki Yonezaki. A Formal Ontology for Business Process Model TAP: Tasks-Agents-Products, Proceedings of the 17th European-Japanese Conference on Information Modeling and Knowledge Bases EJC2007, pp. 294-301, June 2007.
• Souhei Ito, Shigeki Hagihara, Naoki Yonezaki. An Operational Semantics of Program Dependence Graphs for Unstructured Programs, 11th Annual Asian Computing Science Conference (ASIAN 2006), Preliminary Proceedings of 11th Annual Asian Computing Science Conference (ASIAN 2006), pp. 265-272, Dec. 2006.
• Shigeki Hagihara, Naoki Yonezaki. Completeness of Verification methods for Approaching to Realizable Reactive Specifications, 1st Asian Working Conference on Verified Software AWCVS'06, Proceedings of 1st Asian Working Conference on Verified Software AWCVS'06, UNU-IIST Technical Report, Vol. 348, pp. 242-257, Oct. 2006.  公式リンク  
  
• Ashraf Bhery, Shigeki Hagihara, Naoki Yonezaki. A Formal System for Analysis of Cryptographic encryption and Their Security properties, 2nd International Symposium on Software Security 2003, Software Security - Theories and Systems, Lecture Notes in Computer Science, Springer, Vol. 3233, pp. 87-112, June 2004.
• Ashraf Bhery, Shigeki Hagihara, Naoki Yonezaki. A Formal Analysis of Symmetric Encryption and Keyed and Keyed Hash Function, The 46th IEEE International Midwest Symposium On Circuits & Systems, Vol. 2, pp. 774-777, Dec. 2003.
• Ashraf Bhery, Shigeki Hagihara, Naoki Yonezaki. The Characterization of Cryptographic Primitives and Their Security Properties, Proceedings of the Ninth International Conference on Distributed Multimedia Systems, pp. 636-642, Sept. 2003.
• Ashraf Bhery, Shigeki Hagihara, Naoki Yonezaki. Judgment Deduction System of Asymmetric Encryption Scheme (JDE-system), Pre-Proceeding of WISA 2003, The 4th International Workshop on Information Security Applications, pp. 639-649, Aug. 2003.
• ETSUYA SHIBAYAMA, Shigeki Hagihara, Naoki Kobayashi, Shin-ya Nishizaki, Kenjiro Taura, Takuo Watanabe. AnZenMail: A Secure and Certified E-mail System, Lecture Notes in Computer Science (Software Security: Theories and Systems), Vol. 2609, pp. 201-216, 2003.
• Shigeki Hagihara, Naoki Yonezaki. Resolution Method for Modal Logic with Well-founded Frames, 13th International Workshop, CSL'99, 8th Annual Conference of the EACSL, Computer Science Logic, Lecture Notes in computer Science, Springer, Vol. 1683, pp. 277-291, Sept. 1999.
• Shigeki Hagihara, Naoki Yonezaki. Unification-based proof method for modal logic with well-founded frames, International Conference, TABLEAUX'99, Automated Reasoning with Analytic Tableaux and Related Methods: Position Papers, Technical Report, Institute for Programming and Logics, Department of Computer Science, University at Albany - SUNY, Vol. 99, No. 1, pp. 71-85, June 1999.
• Shigeki Hagihara, Naoki Yonezaki. A connection based proof method for modal logic restricted to discrete frames, Fifteenth International Joint Conference on Artificial Intelligence, Poster Session Abstracts, pp. 99, Aug. 1997.

国内会議発表 (査読有り)

• 冨田尭, 上野篤史, 萩原茂樹, 島川昌也, 米崎直樹. 可能な限り仕様を満たすリアクティブシステムの合成, 第22回 ソフトウェア工学の基礎ワークショップ FOSE 2015, ソフトウェア工学の基礎XXII, 日本ソフトウェア科学会 FOSE 2015, 近代科学社, pp. 77-86, Nov. 2015.
• 萩原茂樹, 江川直毅, 島川昌也, 米崎直樹. 強充足不能なリアクティブシステム仕様における欠陥範囲の特定, 第20回 ソフトウェア工学の基礎ワークショップ FOSE 2013, ソフトウェア工学の基礎XX, 日本ソフトウェア科学会 FOSE 2013, 近代科学社, pp. 143-152, Nov. 2013.
• 望月翔平, 島川昌也, 萩原茂樹, 米崎直樹. LTL式からBuchiオートマトンへの高速な変換法, 第19回 ソフトウェア工学の基礎ワークショップ FOSE 2012, ソフトウェア工学の基礎XIX, 日本ソフトウェア科学会 FOSE 2012, 近代科学社, pp. 91-100, Dec. 2012.
• 新井貴大, 島川昌也, 萩原茂樹, 米崎直樹. 時間論理で記述された仕様からのプログラム自動抽出による組み込みシステム構成手法, ソフトウェア工学の基礎XVIII, 日本ソフトウェア科学会 FOSE2011, pp. 151-156, Nov. 2011.
• 萩原茂樹, 北村佑介, 島川昌也, 米崎直樹. リアクティブシステム仕様を実現可能にするための環境制約の抽出, ソフトウェア工学の基礎XVI, 日本ソフトウェア科学会 FOSE2009, pp. 37-48, Nov. 2009.
• 宮本佑樹, 安藤崇央, 萩原茂樹, 米崎直樹. タブロー証明器の実装におけるBDDの利用について, 第五回システム検証の科学技術シンポジウム, 第五回システム検証の科学技術シンポジウム予稿集, pp. 127-138, Nov. 2008.
• 北村佑介, 島川昌也, 萩原茂樹, 米崎直樹. リアクティブシステム仕様の外部環境制約について, 第五回システム検証の科学技術シンポジウム, 第五回システム検証の科学技術シンポジウム予稿集, pp. 7-18, Nov. 2008.
• 島川昌也, 萩原茂樹, 米崎直樹. リアクティブシステム仕様の強充足可能性判定問題の計算量について, 第4回システム検証の科学技術シンポジウム予稿集, pp. 21-29, Nov. 2007.
• 島川昌也, 萩原茂樹, 米崎直樹. リアクティブシステムを対象とした様々な実行時検証概念の形式化とその判定アルゴリズムの完全性, 第二回システム検証の科学技術シンポジウム予稿集, pp. 246-259, Oct. 2005.  公式リンク  
  
• 萩原茂樹, 米崎直樹. Mullerオートマトンを用いたリアクティブシステムの仕様検証法とその完全性, 第二回システム検証の科学技術シンポジウム予稿集, pp. 52-63, Oct. 2005.  公式リンク  
  

国際会議発表 (査読なし・不明)

• Shigeki Hagihara. To develop software without flaws, Workshop on Computation: Theory and Practice (WCTP2016), Sept. 2016.
• Hiroaki Oguro, Shigeki Hagihara, Naoki Yonezaki. A Formal System for Analysis of an Oblivious Transfer Protocol, The 4th Franco-Japanese Computer Security Workshop, Dec. 2008.
• Souhei Ito, Shigeki Hagihara, Naoki Yonezaki. An Ontology for Business Process Model TAP: Tasks-Agents-Products, Proceedings of International Symposium on Large-scale Knowledge Resources (LKR2007), pp. 227-232, Mar. 2007.
• Souhei Ito, Shigeki Hagihara, Naoki Yonezaki. Formalization of process optimization knowledge - An application to code optimization -, International Symposium on Large-scale Knowledge Resources (LKR2006), Proceedings of International Symposium on Large-scale Knowledge Resources (LKR2006), pp. 179-182, Mar. 2006.
• Shigeki Hagihara, Takayoshi Sanui, Naoki Yonezaki. Formal Construction of Security Protocols, 2nd International Workshop on Foundations for Secure/Survivable Systems and Networks, 2nd International Workshop on Foundations for Secure/Survivable Systems and Networks, Oct. 2001.
• Shigeki Hagihara, Takayoshi Sanui, Naoki Yonezaki. Formal Construction of Security Protocols, 公開シンポジウム 「安全な社会基盤を支えるソフトウェア技術」, Sept. 2001.
• Shigeki Hagihara, Naoki Yonezaki. Resolution calculus for Modal logic of finite frames, 1st International Workshop on Specification and Verification of Timed Systems (IWTS'99), 1st International Workshop on Specification and Verification of Timed Systems (IWTS'99), Mar. 1999.

国内会議発表 (査読なし・不明)

• 島川 昌也, 萩原 茂樹, 米崎 直樹. リアクティブシステム仕様の実現可能性に関する非有界検査の効率化に向けて, 第14回ディペンダブルシステムワークショップ DSW2016, Dec. 2016.
• 冨田尭, 萩原茂樹, 島川昌也, 米崎直樹. 実現可能性の必要条件に基づいた不完全リアクティブシステム合成, 日本ソフトウェア科学会第32回大会講演論文集, Sept. 2015.
• 上野篤史, 冨田尭, 島川昌也, 萩原茂樹, 米崎直樹. 環境許容性のあるリアクティブシステム合成法, 電子情報通信学会ソフトウェアサイエンス研究会, 信学技報, Vol. 114, No. 510, pp. 7-12, Mar. 2015.
• 冨田尭, 上野篤史, 萩原茂樹, 米崎直樹. 協調的リアクティブシステムの合成手法, 日本ソフトウェア科学会第31回大会講演論文集, Sept. 2014.
• 萩原茂樹, 江川直毅, 島川昌也, 米崎直樹. リアクティブシステム仕様の極小強充足不能部分計算に関する考察, 情報処理学会第99回プログラミング研究発表会, June 2014.
• 長利健治, 萩原茂樹, 米崎直樹. 実現可能性判定を高速化するための仕様の特徴量に基づいた仕様分割手法, 2014年電子情報通信学会総合大会, 電子情報通信学会2014年総合大会講演論文集, 情報・システム講演論文集1, D-3-2, pp. 17, Mar. 2014.
• 上野篤史, 望月翔平, 島川昌也, 萩原茂樹, 米崎直樹. LTL式で記述されたリアクティブシステム仕様の高速な実現可能性判定器の実装, 第20回ソフトウェア工学の基礎ワークショップFOSE2013, Nov. 2013.
• 長利健治, 室岡拓弥, 萩原聖貴, 安藤崇央, 島川昌也, 伊藤宗平, 萩原茂樹, 米崎直樹. 記述性を重視したリアクティブシステム用仕様記述言語T, 第20回ソフトウェア工学の基礎ワークショップFOSE2013, Nov. 2013.
• 冨田尭, 山崎徹郎, 萩原茂樹, 米崎直樹. 確率的環境下において平均利得時間論理仕様を実現する最適マルコフ決定過程の自動合成法, 日本ソフトウェア科学会第30回大会講演論文集, Sept. 2013.
• 上野篤史, 望月翔平, 島川昌也, 萩原茂樹, 米崎直樹. LTL式で記述されたリアクティブシステム仕様の高速な実現可能性判定器の実装に関する研究, 日本ソフトウェア科学会第30回大会講演論文集, Sept. 2013.
• 冨田尭, 萩原茂樹, 米崎直樹. Mean-Payoff制約を記述可能な線形時間論理, 日本ソフトウェア科学会第29回大会講演論文集, Aug. 2012.
• 樋浦信, 冨田尭, 萩原茂樹, 伊藤宗平, 米崎直樹. 条件付頻度を扱えるように拡張したLTLによるリアクティブシステム仕様の充足可能性判定, ディペンダブルシステムワークショップ & シンポジウム (DSW & DSS 2011), Dec. 2011.
• 冨田尭, 萩原茂樹, 伊藤宗平, 樋浦信, 米崎直樹. 頻度オペレータを導入した線形時間論理に対する統計的手法を用いた確率的モデル検査, 日本ソフトウェア科学会第28回大会講演論文集, Sept. 2011.
• 篠崎隆宏, 関嶋政和, 萩原茂樹, 古井貞熙. 純粋関数型言語を用いた超コンパクトデコーダの開発, 情報処理学会, Apr. 2011.
• Takahiro Shinozaki, Masakazu Sekijima, Shigeki Hagihara, Sadaoki Furui. A compact speech decoder based on pure functional programming, IPSJ-SIGPRO, Manuscript for presentation at IPSJ-SIGPRO, 25 April 2011., 2010-5, 6, Apr. 2011.
• 萩原茂樹, 小黒博昭, 米崎直樹. 暗号文間の関係情報認知可能性に関する論理体系, 情報処理学会第73回全国大会講演論文集, Vol. 1, pp. 233-234, Mar. 2011.
• 小黒博昭, 萩原茂樹, 米崎直樹. 紛失通信プロトコルの解析のための可能世界意味論に基づく形式体系, 情報処理学会第73回全国大会講演論文集, Vol. 3, pp. 439-440, Mar. 2011.
• 冨田尭, 萩原茂樹, 樋浦信, 伊藤宗平, 米崎直樹. 頻度オペレータを導入したProbabilictic CTLとそのモデル検査アルゴリズム, 情報処理学会第73回全国大会講演論文集, Vol. 1, pp. 235-236, Mar. 2011.
• 伊藤宗平, 泉直子, 萩原茂樹, 米崎直樹. 時間論理による仕様記述を用いた遺伝子ネットワークの定性的振る舞い解析, 情報処理学会第73回全国大会講演論文集, Vol. 1, pp. 231-232, Mar. 2011.
• 島川昌也, 萩原茂樹, 米崎直樹. 実現可能性判定コスト削減のための無限ゲーム単純化手法, 日本ソフトウェア科学会第27回大会講演論文集, Sept. 2010.
• 萩原茂樹, 小黒博昭, 米崎直樹. 暗号文間の関係情報を推論する体系に対する可能世界意味論, 日本ソフトウェア科学会第27回大会講演論文集, Sept. 2010.
• 小黒博昭, 萩原茂樹, 米崎直樹. 紛失通信プロトコルを解析する形式体系の意味論, 日本ソフトウェア科学会第27回大会講演論文集, Sept. 2010.
• 篠崎 隆宏, 関嶋 政和, 萩原 茂樹, 古井 貞熙. 柔軟でコンパクトな純粋関数型デコーダの検討, 日本音響学会2010年秋季研究発表会, 日本音響学会2010年秋季講演論文集, 日本音響学会, No. 1-Q-26, pp. 181-182, Sept. 2010.
• 安藤崇央, 萩原茂樹, 米崎直樹. タブロー証明器の実装における SAT solver の利用について, 日本ソフトウェア科学会第26回大会講演論文集, Sept. 2009.
• 島川昌也, 萩原茂樹, 米崎直樹. 実現可能性判定コスト削減のためのLTL構文の制限とそれによる仕様の判定法, 日本ソフトウェア科学会第26回大会講演論文集, Sept. 2009.
• 伊藤宗平, 泉 直子, 萩原茂樹, 米崎直樹. 時間論理LTLの充足可能性判定を用いた遺伝子ネットワークの解析, 日本ソフトウェア科学会第26回大会講演論文集, Sept. 2009.
• 萩原聖貴, 安藤崇央, 島川昌也, 伊藤宗平, 萩原茂樹, 米崎直樹. 記述性を重視したリアクティブシステム用仕様記述言語T, 日本ソフトウェア科学会第26回大会講演論文集, Sept. 2009.
• 安藤崇央, 宮本佑樹, 萩原茂樹, 米崎直樹. 分散オブジェクト技術を利用した段階的充足可能性判定器の実装, 日本ソフトウェア科学会第25回大会講演論文集, Sept. 2008.
• 島川昌也, 萩原茂樹, 米崎直樹. SAT Solverを用いたリアクティブシステム仕様の有界強充足可能性判定, 日本ソフトウェア科学会第25回大会講演論文集, Sept. 2008.
• 小黒博昭, 萩原茂樹, 米崎直樹. 記号論的暗号解析を用いた Oblivious Transfer プロトコルの解析, 日本ソフトウェア科学会第25回大会講演論文集, Sept. 2008.
• 冨田 尭, 泉 直子, 萩原茂樹, 米崎直樹. 量的関係を考慮した生体内の阻害・活性化機能の形式相互作用オントロジー, 日本ソフトウェア科学会第25回大会講演論文集, Sept. 2008.
• 小黒博昭, 萩原茂樹, 米崎直樹. 記号論的暗号解析を用いた Oblivious Transfer プロトコルの解析, コンピュータセキュリティシンポジウム2007 (CSS2007) 論文集, 情報処理学会シンポジウムシリーズ, Vol. 2007, No. 10, pp. 655-660, Oct. 2007.
• 伊藤宗平, 萩原茂樹, 米崎直樹. ビジネスプロセスモデルTAPの形式オントロジーとその応用, 日本ソフトウェア科学会第24回大会講演論文集, Sept. 2007.
• 安藤崇央, 萩原茂樹, 米崎直樹. 分散オブジェクト技術を利用した分散タブロー証明器の実装, 日本ソフトウェア科学会第24回大会講演論文集, Sept. 2007.
• 萩原茂樹, 小黒博昭, 米崎直樹. 暗号文から得られる部分情報に関する推論体系とその計算論に基づく意味, 日本ソフトウェア科学会第24回大会講演論文集, Sept. 2007.
• 秋山卓見, 泉直子, 萩原茂樹, 米崎直樹. 形式オントロジーに基づく遺伝子調節のための数値モデル, 情報処理学会研究報告, Vol. 2007, No. 21, pp. 71-78, Mar. 2007.
• 伊藤宗平, 萩原茂樹, 米崎直樹. 中間コードを表すプログラム依存グラフの操作的意味, 日本ソフトウェア科学会第23回大会, 日本ソフトウェア科学会第23回大会講演論文集, Sept. 2006.
• 島川昌也, 萩原茂樹, 米崎直樹. 仕様の自動検証に適したLTLフラグメント ― 実現集合を表す決定性オートマトン構成の立場から―, 日本ソフトウェア科学会第23回大会, 日本ソフトウェア科学会第23回大会講演論文集, Sept. 2006.
• 伊藤宗平, 萩原茂樹, 米崎直樹. 意味的制約の書き換えによるコンパイラのコード最適化, 日本ソフトウェア科学会第２２回大会講演論文集, pp. 407-414, Sept. 2005.
• 佐藤直人, 萩原茂樹, 米崎直樹. 二者間データ通信を安全に行うプロトコルの自動生成法, 日本ソフトウェア科学会第２２回大会講演論文集, pp. 109-118, Sept. 2005.
• 佐藤直人, 萩原茂樹, 米崎直樹. 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法, 情報処理学会研究報告, Vol. 2005, No. 33, pp. 157-162, Mar. 2005.
• 萩原茂樹, ラッタナウォンナラーカリン, 米崎直樹. 投票プロトコルの安全性の検証, 日本ソフトウェア科学会第21回大会講演論文集, pp. 314-318, Sept. 2004.
• 島川昌也, 萩原茂樹, 米崎直樹. 実時間論理により記述された動作仕様の実行時検証手続き, 日本ソフトウェア科学会第21回大会講演論文集, pp. 179-183, Sept. 2004.
• 関戸達彦, 萩原茂樹, 米崎直樹. 並行プログラムの論理式への変換によるコードレベル検証方式, 日本ソフトウェア科学会第21回大会講演論文集, pp. 174-178, Sept. 2004.
• 伊藤宗平, 萩原茂樹, 米崎直樹. 最適条件の時間論理記述を用いたモデル生成器によるコード最適化, 日本ソフトウェア科学会第20回記念大会論文集, Sept. 2003.
• 佐藤直人, 萩原茂樹, 米崎直樹. プロトコルの構造要件に関する推論を利用したセキュリティプロトコルの自動生成, 日本ソフトウェア科学会第20回記念大会論文集, Sept. 2003.
• 萩原茂樹, 米崎直樹. オークションにおける公平性とその検証, 日本ソフトウェア科学会第20回大会講演論文集, Sept. 2003.
• Ashraf Bhery, Shigeki Hagihara, NAOKI YONEZAKI. A Formal System for Analysis of Cryptographic Primitives and their Security Properties, 20th Conference Proceedings Japan Society for Software Science and Technology, Sept. 2003.
• Ashraf Moustafa Bhery, Shigeki Hagihara, Naoki Yonezaki. A new deduction system for cryptographic primitives and their security properties, IPSJ SIG Technical Reports, Vol. 2003, No. 74, pp. 31-38, July 2003.
• 萩原茂樹, 米崎直樹. 入札プロトコルの形式的検証, 日本ソフトウェア科学会第19回大会講演論文集, Sept. 2002.
• 畑山研, 萩原茂樹, 米崎直樹. Spi計算の型付けによる公開鍵暗号方式を用いたプロトコルのメッセージ認証の検証, 情報処理学会研究報告, Vol. 2002, No. 43, pp. 25-30, May 2002.
• 畑山研, 萩原茂樹, 米崎直樹. Spi-calculusを用いたプロトコルの認証に関する性質の検証, 日本ソフトウェア科学会第18回大会論文集, Sept. 2001.
• 讃井崇喜, 萩原茂樹, 米崎直樹. セキュリティプロトコルの自動設計アルゴリズム, 日本ソフトウェア科学会第18回大会論文集, Sept. 2001.
• 萩原茂樹, 友石正彦, 米崎直樹. 有礎構造を意味論にもつ様相論理の分解証明法, 日本ソフトウェア科学会第15回大会論文集, pp. 145-148, Sept. 1998.
• 友石正彦, 萩原茂樹, 米崎直樹. 初等的でないフレームを持つ様相論理の統一化による証明法, 情報処理学会第55回全国大会講演論文集, Vol. 2, pp. 559-560, Sept. 1997.
• 萩原茂樹, 米崎直樹. ある種の離散性を仮定した様相論理の統一化による証明方法, 日本ソフトウェア科学会第14回大会論文集, pp. 385-388, Sept. 1997.
• 萩原茂樹, 米崎直樹. 様相論理証明における失敗情報の利用, 日本ソフトウェア科学会第12回大会論文集, pp. 105-108, Sept. 1995.
• 萩原茂樹, 米崎直樹. 証明の失敗から得られる情報を用いる様相論理定理証明戦略, 情報処理学会第50回全国大会講演論文集, Vol. 3, pp. 5-6, Mar. 1995.

その他の論文・著書など

• 萩原茂樹, 米崎直樹. 記号論及び計算論によるセキュリティ解析の相互関係, 応用数理, Vol. 17, No. 4, pp. 27-37, Dec. 2007.
• 萩原茂樹, 米崎直樹. Abadi-Rogawayによる暗号メッセージの解析手法とその健全性・完全性について, 第7回「代数幾何・数論及び符号・暗号」研究集会報告集, Dec. 2006.

学位論文

• 到達可能関係の無限連鎖に制約を持つ様相論理体系の証明方法に関する研究 ,  本文,  Doctor of Engineering,  Tokyo Institute of Technology,  2000/--/--, 

[ BibTeX 形式で保存 ]    [ 論文・著書をCSV形式で保存 ]    [ 特許をCSV形式で保存 ]