活動

プロジェクト

ソフトウェア形式手法分野のメンバーはこれまでに多数のプロジェクトに参画し研究成果をあげています．

文部科学省関連のプロジェクト

社会基盤としてのセキュアコンピューティングの実現方式の研究 : 科学研究費特定領域研究（Ｂ）（2000年～2004年）
発展機構を備えたソフトウェアの構成原理の研究 : 科学研究費重点領域研究（1996年～1999年）

情報処理振興事業協会の公募プロジェクト

組み込みシステム用基盤ソフトウェアＳＭＡＦの研究開発 : 独創的先進的情報技術研究開発事業（1998年～2001年）
開放型分散環境でのソフトウェア部品検証システムの研究開発 : 独創的先進的情報技術研究開発事業（1999年～2001年）
ネットワーク上で統合された代数仕様言語環境の研究開発 : 創造的ソフトウェア推進事業（1996年～1998年）
インターネット利用コンポーネントソフトウェア管理システム : 高度情報化支援ソフトウェアシーズ育成事業（2001年～2002年）
コンポーネント仕様に基づく高信頼性Ｊａｖａコード生成支援ツール : 高度情報化支援ソフトウェアシーズ育成事業（1999年～2000年）
ＯＤＰトレーダの実行可能仕様とそのラーニングウェアの開発 : 高度情報化支援ソフトウェアシーズ育成事業（1998年～1999年）
動的適応可能なソフトウェアの系統的構成方式と言語の研究開発 : 高度情報化支援ソフトウェアシーズ育成事業（1998年～1999年）

GO TO TOP

学外賞与

2001年 電子情報通信学会北陸支部学生論文賞 村田真一（渡部研究室）
2003年 the best paper of SCI2003 Jianwen Xiang, Kokichi Futatsugi and Yanxiang He: "Fault Tree Analysis of Software Reliability Allocation", Proceedings of 7th World Multiconference on Systemics, Cybernetics and Informatics (SCI 2003), Volume II - Computer Science and Engineering, pp. 460-465, Orlando, USA, July 27-30, 2003

GO TO TOP

国際論文 (2002.4～)

国際会議, 論文誌

2008

Jianwen Xiang, Dines Bjorner, and Kokichi Futatsugi: Formal Digital License Language with OTS/CafeOBJ Method, Proc. of The sixth ACS/IEEE International Conference on Computer Systems and Applications, (AICCSA-08), IEEE Computer Society, 2008.
Kazuhiro Ogata and Kokichi Futatsugi: Simulation-based verification for 　invariant properties in the OTS/CafeOBJ method, Proceedings ofthe 4th　International Refinement Workshop (Refine 2007), ENTCS 201, Elsevier, pp.127-154 (2008).

2007

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.
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, Vol.17, No.6, pp.783-804, World Scientific, 2007.
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.
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, 2007.
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.
Xiaoyi Chen, Jianwen Xiang, Weiqiang Kong and Kokichi Futatsugi: Formalization and Analysis of Public Administration Domain with the OTS/CafeOBJ Method, Proceedings of 3th International Conference on e-Government (ICEG 2007), ISBN: 1-905305-59-1, ACL, pp. 77-86, Sept., 2007.
Xiaoyi Chen, Jianwen Xiang, Dines Bjorner and Kokichi Futatsugi: A License Language Design and Analysis for E-Government, Proceedings of International Conference on Wireless Communications, Networking and Mobile Computing (WiCom 2007), ISBN: 1-4244-1312-5, IEEE, pp. 3445 - 3448, Sept., 2007.
Xiaoyi Chen, Weiqiang Kong and Kokichi Futatsugi: Formal support for e-government system design with transparency consideration, Proceedings of the 1st International Conference on Theory and Practice of Electronic Governance (ICEGOV 2007), ACM, pp. 20-29, 2007.
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).
Masaki Nakamura and Kokichi Futatsugi: On equality predicates in algebraic specification languages, Proceedings of the 4th International Colloquium on Theoretical Aspects of Computing (ICTAC 2007), Lecture Notes in Computer Science 4711,

2006

中村正樹二木厚吉, モジュラーな代数仕様言語のための項書き換えシステム, コンピュータソフトウェア (日本ソフトウェア科学会論文誌)， Vol. 23 No. 3, pp. 35-50, JULY 2006.
Masaki Nakamura, Watanabe, M., Kokichi Futatsugi: A Behavioral Specification of Imperative Programming Languages, IEICE Transactions on Fundamentals of Electronics, Communications anc Computer Sciences (電子情報通信学会論文誌)， Vol. E89-A No. 6, pp. 1558-1565, JUNE 2006.
Jianwen Xiang, Kazuhiro Ogata, Weiqiang Kong and Kokichi Futatsugi: From Fault Tree Analysis to Formal System Specification and Verification with OTS/CafeOBJ，Computer Software, JSSST, (コンピュータソフトウェア(日本ソフトウェア科学会論文誌))，Vol.23, No.3, pp.134-146， 2006．
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 (IJSEKE), Vol. 17, No. 1 (2007) pp.1-30, World Scientific Publishing, 2006.
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.
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.
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.
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.
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.
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.
Kokichi FUTATSUGI, Verifying Specifications with Proof Scores in CafeOBJ (an invited keynote paper at ASE 2006), Proc. of 21st IEEE International Conference on Automated Software Engineering, pp. 3-10, 2006.
Jing Tian, Yoshiteru Nakamori, Jianwen Xiang and Kokichi Futatsugi, Knowledge Management in Academia: Survey, Analysis and Perspective, Int. J. Management and Decision Making, pp. 275-294, Vol. 7, Nos. 2/3, 2006.

2005

Kazuhiro Ogata, Masahiro Nakano, Masaki Nakamura, and Kokichi Futatsugi: Chocolat/SMV: A Translator from CafeOBJ into SMV, Proc. of the 6th Intl. Conf. on Parallel and Distributed Computing, Applications and Technologies, IEEE Computer Society Press, December 2005.
Weiqiang Kong, Kazuhiro Ogata, Takahiro Seino, and Kokichi Futatsugi: A Lightweight Integration of Theorem Proving and Model Checking for System Verification, Proc. of the 12th Asia-Pacific Software Eng. Conf., IEEE Computer Society Press, December 2005.
Kokichi Futatsugi, Joseph Goguen, and Kazuhiro Ogata: Verifying Design with Proof Scores, Proc. of 1st IFIP-WG2.3 Conf. on Verified Software: Tool, Theory, and Experience (electric form), October 2005.
Weiqiang Kong, Kazuhiro Ogata, and Kokichi Futatsugi: Formal Analysis of Workflow Systems with Security Considerations, Proc. of the 17th International Conf. on Software Eng. and Knowledge Eng., pp.531-536, September 2005.
Jianwen Xiang, Kazuhiro Ogata, and Kokichi Futatsugi: Formal Fault Tree Analysis of State Transition Systems, Prceedings of the 5th Intl. Conf. on Quality Software, IEEE Computer Society Press, pp.124-131, September 2005.
Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, and Kokichi Futatsugi: Automatic Verification of the STS Authentication Protocol with Creme, Proc. of the 2005 Intl. Technical Conf. on Circuits/Systems, Computers and Communications, pp.15-16, July 2005.
Kazuhiro Ogata and Kokichi Futatsugi: Proof Score Approach to Verification of Liveness Properties, Proc. of the 17th Intl. Conf. on Software Eng. and Knowledge Eng., pp.608-613, July 2005.
Jittisak Senachak, Takahiro Seino, Kazuhiro Ogata, and Kokichi Futatsugi: Provably Correct Translation from CafeOBJ into Java, Proc. of the 17th Intl. Conf. on Software Eng. and Knowledge Eng., pp.614-619, July 2005.
Masaki Nakamura, Masahito Watanabe, and Kokichi Futatsugi: A behavioral specification of Imperative Programming Languages, The 2005 Intl. Technical Conf. On Circuits/System, Computers and Communications, pp. 403-404, July 2005.
Kazuhiro Ogata and Kokichi Futatsugi: Equational Approach to Formal Analysis of TLS, Proc. of the 25th Intl. Conf. on Distributed Computing Systems, IEEE Computer Society Press, pp.795-804, June 2005.
Takahiro Seino, Kazuhiro Ogata, and Kokichi Futatsugi: Mechanically Supporting Case Analysis for Verification of Distributed Systems, Journal of Pervasive Computing and Communications, 1(2): 135-145, Troubador, June 2005.
Takahiro Seino, Kazuhiro Ogata, and Kokichi Futatsugi: A Toolkit for Generating and Displaying Proof Scores in the OTS/CafeOBJ Method, Proc. of the 6th Intl. Workshop on Rule-Based Programming, ENTCS, Elsevier, April 2005.
中村正樹, 緒方和博, 二木厚吉, 項書き換えシステムにおける可簡約演算子とその応用, 情報処理学会論文誌：プログラミング, vol.46, No.SIG 6 (PRO25), pp.47-59, 2005年4月.

2004

Kazuhiro Ogata and Kokichi Futatsugi: Formal Analysis of the NetBill Electronic Commerce Protocol, Proc. of the 2nd Intl. Symp. on Software Security, LNCS 3233, Springer, pp.45-64, November 2004.
Jianwen Xiang, Kokichi Futatsugi, and Yanxiang He: Formal Fault Tree Construction Model and Specification, Proc. of The 8th IASTED Intl. Conf. SOFTWARE ENG. AND APPLICATIONS 2004, pp.374-381, Nov. 2004.
中村正樹, 二木厚吉, 項書き換えシステムにおける可簡約演算子とその応用, 情報科学技術レターズ vol.3 (FIT2004)，pp.13-14, 2004年9月.
Takahiro Seino, Kazuhiro Ogata, and Kokichi Futatsugi: Supporting Case Analysis with Algebraic Specification Languages, Proc. of the 4th Intl. Conf. on Computer and Information Technology, IEEE Computer Society Press, pp. 1100-1107, September 2004.
Weiqiang Kong, Kazuhiro Ogata, Jianwen Xiang, and Kokichi Futatsugi: Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol, Proc. of the 4th Intl. Conf. on Computer and Information Technology, IEEE Computer Society Press, pp.1100-1107, September 2004.
Kazuhiro Ogata and Kokichi Futatsugi: Equational Approach to Formal Verification of SET, Proc. of the 4th Intl. Conf. on Quality Software, IEEE Computer Society Press, pp.50-59, September 2004.
Jianwen Xiang, Kokichi Futatsugi, and Yanxiang He: Fault Tree and Formal Methods in System Safety Analysis, Proc. of The 4th Intl. Conf. on Computer and Information Technology 2004, IEEE Computer Society Press, pp.1108-1115, Sep. 2004.
Kazuhiro Ogata, Daigo Yamagishi, Takahiro Seino, and Kokichi Futatsugi: Modeling and Verification of Hybrid Systems Based on Equations, Proc. of the IFIP 18th World Computer Congress TC10 Working Conf. on Distributed and Parallel Embedded Systems, Kluwer, pp.43-52, August 2004.
Jianwen Xiang, Kokichi Futatsugi, and Yanxiang He: Formal Fault Tree Construction and System Safety Analysis, Proc. of IASTED Intl. Conf. on Software Eng., pp.378-384, Feb.2004.

2003

Kazuhiro Ogata and Kokichi Futatsugi: Proof scores in the OTS/CafeOBJ method, Proc. of the 6th IFIP WG6.1 Intl. Conf. on Formal Methods for Open Object-Based Distributed Systems, LNCS 2884, pp.170-184, Springer, November 2003.
Toshimi Sawada, Kouichi Kishida, and Kokichi Futatsugi: Past, Present, and Future of SRA Implementation of CafeOBJ, Proc. of Intl. Symposium of Formal Methods Europe 2003, LNCS 2805, pp.7-17, September 2003.
清野貴博, 緒方和博, 二木厚吉: 項書換えを用いた安全性検証の組織化，コンピュータソフトウェア, Vol.20, NO.5, pp.32-45, 2003年9月.
Razvan Diaconescu, Kazuhiro Ogata, and Kokichi Futatsugi: CafeOBJ: Logical foundation and methodologies, Computing and Informatics, Vol.22, pp.257-283, August 2003.
Kazuhiro Ogata and Kokichi Futatsugi: Flaw and modification of the iKP electronic payment protocols. Information Processing Letters, Vol.86, pp.57-62, Springer, April 2003.
緒方和博, 二木厚吉: 書き換えによるセキュリティプロトコルの帰納的検証，コンピュータソフトウェア, Vol.20, NO.3, pp 54-72, 2003年3月.
Kazuhiro Ogata and Kokichi Futatsugi: Formal verification of the Horn-Preneel micropayment protocol, Proc. of the 4th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation, LNCS 2575, Springer, pp.238-252, Jan. 2003.
Jianwen Xiang, Kokichi Futatsugi and Yanxiang He: Fault Tree Analysis of Software Reliability Allocation, Proceedings of 7th World Multiconference on Systemics, Cybernetics and Informatics (SCI 2003), Volume II - Computer Science and Engineering, pp. 460-465, Orlando, USA, July 27-30, 2003 (the best paper of SCI2003)
Jianwen Xiang, Yanxiang He, Kokichi Futatsugi, and Weiqiang Kong Constructing Projection Frequent Pattern Tree for Efficient Mining, Wuhan University Journal of Natural Sciences, Vol. 8 No. 2A, pp. 351-357, June 2003
Kazuhiro Ogata and Kokichi Futatsugi: Formal verification of the Horn-Preneel micropayment protocol, Proc. of the 4th Int'l Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2003), LNCS 2575, Springer, pp.238-252, Jan. 2003

2002

Kazuhiro Ogata and Kokichi Futatsugi: Formal analysis of the iKP electronic payment protocols, Proc. of Int'l Symposium on Software Security, LNCS 2609 (Hot Topics, Software Security - Theories and Systems), Springer, pp.-, Nov.2002
Kazuhiro Ogata and Kokichi Futatsugi: Rewriting-based verification of authentication protocols, Proc. of 4th Int'l Workshop on Rewriting Logic and its Applications (WRLA 2002), Electronic Notes in Theoretical Computer Science, Vol.71, Elsevier Science Publishers, Sep. 2002
Kazuki Munakata and Kokichi Futatsugi, An Algebraic Approach to Validation of Class Diagram with Constraints, Proc of ITC-CSCC2002, vol2 pp.920-923, July 2002.

国内発表論文（査読有り）

中村正樹, 二木厚吉, モジュラーな代数仕様言語のための項書き換えシステム，第二回システム検証の科学技術シンポジウム， pp. 106-121, October 2005.
Weiqiang Kong, Kazuhiro Ogata, and Kokichi Futatsugi: Formal Modeling and Verification of Workflows with Security Considerations, Proc. of The 2nd Information Technique Symposium of System Verification, pp.135-149, October 2005. (第二回システム検証の科学技術シンポジウム)
J. Xiang, K. Ogata, W. Kong, and K. Futatsugi. From safety analysis to formal system specification and verification with OTS/CafeOBJ. In Proc. of the Second Symposium on Science and Technology for System Verification, pp. 64-78, October 2005. (第二回システム検証の科学技術シンポジウム)
中野昌弘, 中村正樹, 緒方和博, 二木厚吉, SMVによるOTS/CafeOBJ仕様のモデル検査, ソフトウェア工学の基礎XI 日本ソフトウェア科学会 FOSE2004, pp.129-140, 2004年11月.
中村正樹, 二木厚吉: 構造的代数仕様のための等価述語の提案と実装, ソフトウェア工学の基礎XI 日本ソフトウェア科学会 FOSE2004, pp.117-128, 2004年11月.
清野貴博, 加藤淳, 緒方和博, 二木厚吉, 書き換えによるOtway-Rees 認証プロトコルの検証, ソフトウェア工学の基礎XI 日本ソフトウェア科学会 FOSE2004, pp.153-155, 2004年11月.
清野貴博, 緒方和博, 二木厚吉, 項書換えを用いた安全性検証の組織化, ソフトウェア工学の基礎IX 日本ソフトウェア科学会 FOSE2002, レクチャーノート/ソフトウェア学, 28, pp 107-118, 2002.11
宗像一樹, 二木厚吉, 解析可能なオブジェクトモデルとしての制約付きクラス図, ソフトウェア工学の基礎IX 日本ソフトウェア科学会 FOSE2002, レクチャーノート/ソフトウェア学, 28, , pp 151-154, 2002.11
小池憲史, 二木厚吉, テーブルを用いた形式仕様, ソフトウェア工学の基礎IX 日本ソフトウェア科学会 FOSE2002, レクチャーノート/ソフトウェア学, 28, pp 187-190, 2002.11
中村正樹, 二木厚吉, CafeOBJにおける書き換えエンジンの停止性, ソフトウェア工学の基礎IX 日本ソフトウェア科学会 FOSE2002, レクチャーノート/ソフトウェア学, 28, pp 191-194, 2002.11

国内発表論文（査読無し）

Weiqiang Kong, Kazuhiro Ogata, and Kokichi Futatsugi: Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System, Research Report, IS-RR-2007-004, JAIST, March 2007.
有本泰仁，二木厚吉: ドメインの形式記述と検証，電子情報通信学会研究報告 SS2007-15, pp.35-40, 2007
二木厚吉，緒方和博，有本泰仁：法令対象ドメインの形式記述と検証，片山卓也編「法令工学の提案」, JAIST Press, 第４章（pp71-93）, 2007.
中村正樹, 二木厚吉: 実行可能な代数仕様の停止性証明について, 情報科学技術レターズ (FIT2007)，pp.27-30, 2007.9.
Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi: complete specification transformation from OTS/CafeOBJ to OTS/Maude (OTS/CafeOBJからOTS/Maudeへの仕様変換の研究)，電子情報通信学会技術研究報告，信学技報，106(120):1-6，2006．
Weiqiang Kong, Kazuhiro Ogata, Masaki Nakamura and Kokichi Futatsugi: A Review of Induction-Guided Falsification and Towards its Automation, Preliminary Proceedings of the 1st Asian Working Conference on Verified Software (1st AWCVC), pp48-59, 2006.
渡辺真啓, 中村正樹, 二木厚吉, 隠蔽代数に基づく命令型プログラム言語の意味論の記述と検証, 情報科学技術フォーラム FIT2004 一般講演論文集第1分冊, pp.173-174, 2004年9月.
Jitticak Senachak, Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi, Provably Correct Translation from OTS/CafeOBJ Specifications to Java Programs,情報科学技術フォーラム FIT2004 一般講演論文集第1分冊, pp.175-176, 2004年9月.
原光太朗, 緒方和博, 中村正樹, 二木厚吉, 代数仕様言語CafeOBJ と証明支援系Coq によるSTS プロトコルの形式化と検証, 情報科学技術フォーラム FIT2004 一般講演論文集第1分冊, pp.177-178, 2004年9月.
及部佳代子, 清野貴博, 天野憲樹, 二木厚吉, モバイルエージェント間の柔軟な情報交換を可能にするフレームワークの提案, 第2回情報科学技術フォーラム Forum on Information Technology (FIT2003) 講演論文集, B-041, 2003.9
加藤淳, 中村正樹, 緒方和博, 二木厚吉, 代数仕様言語CafeOBJによるセキュリティプロトコルの形式化, 第2回情報科学技術フォーラム Forum on Information Technology (FIT2003) 講演論文集, B-003, 2003.9
河本孝久, 中村正樹, 二木厚吉, 実行可能なプロセス代数を用いた仕様解析, 第2回情報科学技術フォーラム Forum on Information Technology (FIT2003) 講演論文集, B-004, 2003.9
山岸大悟, 清野貴博, 緒方和博, 二木厚吉, CafeOBJを用いたハイブリッドシステムの形式的な仕様記述と検証 , 第2回情報科学技術フォーラム Forum on Information Technology (FIT2003) 講演論文集, B-002, 2003.9
Masaki Nakamura, Verification by Term Rewriting with the Equality Predicates "==" and "=/=", the 21th Term Rewriting Meeting, Noto Peninsula, Ishikawa, 2002.10
浅羽義之, 中村正樹, 天野憲樹, 二木厚吉, 代数仕様言語CafeOBJのための拡張可能な前処理系, 第1回情報科学技術フォーラム Forum on Information Technology (FIT2002) 一般講演論文集第一分冊, pp 89-90, 2002.9
中野昌弘, 中村正樹, 二木厚吉, 代数仕様言語CafeOBJにおけるモデル検査, 第1回情報科学技術フォーラム Forum on Information Technology (FIT2002) 一般講演論文集第一分冊, pp 91-92, 2002.9

GO TO TOP

学内賞与

博士後期課程修了者：成績優秀賞

2002年松本充広（二木研究室）
1999年天野憲樹（渡部研究室）

博士前期課程修了者：成績優秀賞

2000年松宮千代（二木研究室）
1999年清野貴博（二木研究室）
1998年松本充広（二木研究室）
1996年田中哲（渡部研究室）
1994年宮内興治（渡部研究室）

GO TO TOP

学内論文

博士・修士論文の一部は図書館のページから電子的に取得することができます．

博士論文

2003年	清野貴博
2003年	項書換えを用いた安全性検証の組織化
2002年	松本充広
	Lightweight Formal Methods for Comonent-based Software Development
	中村正樹
	Evaluation Strategies for term rewriting systems
2001年	佐伯豊
2001年	再利用可能な拡張機構を備えた言語処理系
2000年	田中哲
2000年	拡張の合成を容易とするメタレベルアーキテクチャの研究
1999年	天野憲樹
	A Study on a Methodology of Constructing Dynamically Adaptable Software Systems
	飯田周作
	An Algebraic Formal Method for Component based Software Developments
	五百蔵重典
	モジュールシステムの設計と検証に関する研究
1998年	石川洋
1998年	並行自己反映計算の宣言的記述に関する研究

修士論文

2005年	原光太朗
	STSプロトコルの形式化と検証によるCafeOBJとCoqの比較
	渡辺真啓
	隠蔽代数に基づく命令型言語の意味論
2004年	及部佳代子
	モバイルエージェント間の柔軟な情報交換を可能にするフレームワークの設計と実装
	加藤淳
	代数仕様言語CafeOBJによるセキュリティプロトコルの形式化
	河本孝久
	実行可能なプロセス代数系を用いた仕様解析に関する研究
	山岸大悟
	CafeOBJ を用いたハイブリッドシステムの形式的な仕様記述と検証
2003年	浅羽義之
	代数仕様言語CafeOBJのための拡張可能な前処理系
	中野昌弘
	モデル検査を用いたシステム検証の支援に関する研究
2002年	片山仁史
	UML仕様からのコンポーネントソフトウェア生成に関する研究
	櫻井一雅
	条件付順序ソート項書換え系の停止性自動判定に関する研究
	中間貴規
	ビジネスソフトウェアのドメイン分析に基づくコンポーネント化の研究
	橋本吉治
	軽量フォーマルメソッドを利用したコンポーネントソフトウェア向け検証ツールに関する研究
	長谷川信
	耐タンパ・モバイルエージェントを実現するセキュリティ機構の提案と実装
2001年	金城直貴
	セキュリティプロトコルの代数モデルに基づく形式化
	宗像一樹
	振舞仕様によるUMLの意味解析に関する研究
	菅原美樹
	FA(Factory Automation)システムの形式仕様とモデル化に関する研究
	小林一樹
	モバイルエージェントを用いた情報共有システムの設計と構築
	村田真一
	不正なホストの盗み見からモバイルエージェントを保護するセキュリティ機構の提案と実装
2000年	奥村滋
	Java仮想機械の形式仕様とその検証
	松宮千代
	UNIXファイルシステムの振舞仕様
	市山洋乃
	CafeOBJのラーニングシステムのデザインに関する研究
	長坂浩司
	移動エージェントの移動パターンに対応した障害処理機構
	山田聖
	コンパイル時自己反映計算を用いたカスタマイズ可能な言語処理系に関する研究
1999年	兼英樹
	CafeOBJからJavaへの変換と同期記述
	清野貴博
	代数仕様言語CafeOBJによる鉄道信号システムの記述
	川崎大輔
	動的コード生成を用いた適応的移動コードに関する研究
	新堀健治
	信頼性の高い移動エージェントシステムの構成方法
	西川尚宏
	自己反映機構を用いた移動エージェント記述言語
	峯下聡志
	Ambient Calculusを用いた移動エージェントの形式化
1998年	斎藤嗣治
	Parallel TRAMのごみ集めの並列化に関する研究
	平田寛道
	Parallel TRAMを基にした超並列TRAMの実装と評価
	松本充広
	振舞仕様の検証方法に関する研究
	梅原伸年
	CafeOBJによるB-抽象機械モデルの検証法に関する研究
	守田正憲
	実装パターンを導入したメタオブジェクト合成法
	Sihattha Rasphone
	Local Area Information Service Architecture for Mobile Applications
	佐藤徹也
	語彙にもとづくクラスライブラリの構成法について
1997年	浦上貴裕
	パラメータ化プログラミングにおけるモジュール変換に関する研究
	近藤勝
	並列項書換え抽象機械：Parallel TRAMの設計と実装
	杉山智倫
	形式仕様の記述スタイルに関する研究
	阿部修
	Java言語における非同期通信の抽象化
	佐伯豊
	自己反映的逐次プログラミング言語の効率的なコンパイル手法について
1996年	飯田周作
	並行オブジェクト指向モデルに基づく並行分散システムの形式仕様作成法
	五百蔵重典
	AC演算子を含んだ項書換えコンパイラに関する研究
	大原幸一
	弁別ネットを利用した項書き換え抽象機械の設計
	佐藤薫
	形式仕様からの効率的なプログラム導出に関する研究
	海野浩
	形式仕様のライブラリに関する研究
	天野憲樹
	Meta-level Architectureを用いた移動計算機環境を支援する言語処理系の実現
	田中哲
	拡張を容易とするプログラミング言語の研究
	永藤直行
	自己反映的並行計算の操作的意味について
	石本茂
	Bird-Meertens Formalismに基づく関数型言語の超並列計算機上への実現に関する研究
1995年	石川洋
	書き換え論理に基づく並行自己反映計算のモデル化
	浜口正孝
	形式仕様言語OBJによるオブジェクト指向仕様記述
	松原豪
	ガベージコレクションアルゴリズムの並列計算機上での実装
	山岡順一
	値呼びλ計算にもとづくリフレクティブなプログラミング言語の操作的意味論
1994年	菅原太郎
	並行項書き換え計算を実行モデルとする並行オブジェクト指向言語の実現方法に関する研究
	瀬尾明志
	分散環境におけるガベージコレクションの研究
	戸松豊和
	分散メモリ型並列計算機におけるマルチスレッドの実装方式の研究
	中辻康弘
	メタレベルアーキテクチャを用いた分散アルゴリズムの階層的記述方式の研究
	三浦英樹
	並列オブジェクト指向言語処理系の超並列計算機上における実現
	宮内興治
	アプリケーションプログラム自身による動的負荷分散の実現方式

GO TO TOP