Software model checking methods for cloud computing middleware

• Project/Area Number: 23240003
• Research Category: Grant-in-Aid for Scientific Research (A)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: The University of Tokyo
• Principal Investigator: Hagiya Masami 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
• Co-Investigator(Kenkyū-buntansha): ARTHO Cyrille 産業技術総合研究所, 情報セキュリティセンター, 研究員 (30462831) ; YAMAMOTO Mitsuharu 千葉大学, 大学院理学研究科, 准教授 (00291295) ; TANABE Yoshinori 鶴見大学, 文学部, 教授 (60443199) ; YOKOYAMA Shigetoshi 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (10600968)
• Research Collaborator: WEITL Franz ; POTTER Richard ; LEUNGWATTANAKIT Watcharin
• Project Period (FY): 2011-04-01 – 2016-03-31
• Project Status: Completed (Fiscal Year 2015)
• Budget Amount: ¥48,360,000 (Direct Cost: ¥37,200,000、Indirect Cost: ¥11,160,000); Fiscal Year 2015: ¥9,230,000 (Direct Cost: ¥7,100,000、Indirect Cost: ¥2,130,000); Fiscal Year 2014: ¥9,230,000 (Direct Cost: ¥7,100,000、Indirect Cost: ¥2,130,000); Fiscal Year 2013: ¥9,230,000 (Direct Cost: ¥7,100,000、Indirect Cost: ¥2,130,000); Fiscal Year 2012: ¥9,230,000 (Direct Cost: ¥7,100,000、Indirect Cost: ¥2,130,000); Fiscal Year 2011: ¥11,440,000 (Direct Cost: ¥8,800,000、Indirect Cost: ¥2,640,000)
• Keywords: 仕様記述・仕様検証 / ソフトウェアモデル検査 / クラウドコンピューティング

Outline of Final Research Achievements

We have developed methods of software verification for network applications that are typical in cloud computing environments. Our software model checking tool has been enhanced so that it can handle various protocols and application configuration. We also have developed a novel tool based on model base testing so that we can verify a wider range of applications. The usefulness of the tools has been confirmed by experiments with network applications such as Zookeeper, software for coordination of distributed processes in cloud computing environments.

Research Products

• [Journal Article] Guiding random test generation with program analysis (2016)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Johannes Gmeiner, Rudolf Ramler
  • Journal Title: Proc Software Engineering 2016 Volume: 2016 Pages: 15-16
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] Cardinality of UDP Transmission Outcomes (2015)
  • Author(s): Franz Weitl, Nazim Sebih, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Mitsuharu Yamamoto
  • Journal Title: Proc 1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications Volume: 2015 Pages: 120-134
  • DOI: 10.1007/978-3-319-25942-0_8
  • ISBN: 9783319259413, 9783319259420
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Using Checkpointing and Virtualization for Fault Injection (2015)
  • Author(s): Cyrille Artho, Kuniyasu Suzaki, Masami Hagiya, Watcharin Leungwattanakit, Richard Potter, Eric Platon, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
  • Journal Title: International Journal of Networking and Computing Volume: 5 Issue: 2 Pages: 347-372
  • DOI: 10.15803/ijnc.5.2_347
  • NAID: 130005091738
  • ISSN: 2185-2839, 2185-2847
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Software Model Checking of UDP-based Distributed Applications (2015)
  • Author(s): Nazim Sebih, Masami Hagiya, Franz Weitl, Mitsuharu Yamamoto, Cyrille Artho, Yoshinori Tanabe
  • Journal Title: International Journal of Networking and Computing Volume: 5 Pages: 373-402
  • NAID: 130005091737
  • Peer Reviewed / Open Access / Acknowledgement Compliant
• [Journal Article] Model-Based Testing of Stateful APIs with Modbat (2015)
  • Author(s): Cyrille Artho, Martina Seidl, Quentin Gros, Eun-Hye Choi, Takashi Kitamura, Akira Mori, Rudolf Ramler, Yoriyuki Yamagata
  • Journal Title: Proc 30th IEEE/ACM International Conference on Automated Software Engineering Volume: 2015 Pages: 858-863
  • DOI: 10.1109/ase.2015.95
  • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] GRT: Program-Analysis-Guided Random Testing (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Johannes Gmeiner, Rudolf Ramler
  • Journal Title: Proc 30th IEEE/ACM International Conference on Automated Software Engineering Volume: 2015 Pages: 212-223
  • DOI: 10.1109/ase.2015.49
  • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] GRT: An Automated Test Generator Using Orchestrated Program Analysis (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Johannes Gmeiner, Rudolf Ramler
  • Journal Title: Proc 30th IEEE/ACM International Conference on Automated Software Engineering Volume: 2015 Pages: 842-847
  • DOI: 10.1109/ase.2015.102
  • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] Domain-Specific Languages with Scala (2015)
  • Author(s): Cyrille Artho, Klaus Havelund, Rahul Kumar, Yoriyuki Yamagata
  • Journal Title: Proc 17th International Conference on Formal Engineering Methods Volume: 2015 Pages: 1-16
  • DOI: 10.1007/978-3-319-25423-4_1
  • ISBN: 9783319254227, 9783319254234
  • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
• [Journal Article] GRT at the SBST 2015 Tool Competition (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
  • Journal Title: Proc 8th IEEE/ACM International Workshop on Search-Based Software Testing Volume: 2015 Pages: 48-51
  • DOI: 10.1109/sbst.2015.19
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] Depth-First Heuristic Search for Software Model Checking (2015)
  • Author(s): Jun Maeoka, Yoshinori Tanabe, Fuyuki Ishikawa
  • Journal Title: Proc 14th IEEE/ACIS International Conference on Computer and Information Science Volume: 2015 Pages: 75-96
  • DOI: 10.1007/978-3-319-23467-0_6
  • ISBN: 9783319234663, 9783319234670
  • Peer Reviewed
• [Journal Article] A Knoppix-based demonstration environment for JPF (2014)
  • Author(s): Richard Potter, Cyrille Artho, Kuniyasu Suzaki, Masami Hagiya
  • Journal Title: ACM SIGSOFT Software Engineering Notes Volume: 39 Issue: 1 Pages: 1-5
  • DOI: 10.1145/2557833.2560574
  • Acknowledgement Compliant
• [Journal Article] Software Model Checking of UDP-based Distributed Applications (2014)
  • Author(s): Nazim Sebih, Franz Weitl, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
  • Journal Title: Proc. Second International Symposium on Computing and Networking Volume: 2014 Pages: 96-105
  • DOI: 10.1109/candar.2014.66
  • NAID: 130005091737
  • Peer Reviewed
• [Journal Article] Using Checkpointing and Virtualization for Fault Injection (2014)
  • Author(s): Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Eric Platon, Richard Potter, Kuniyasu Suzaki, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
  • Journal Title: Proc. Second International Symposium on Computing and Networking Volume: 2014 Pages: 144-150
  • DOI: 10.1109/candar.2014.45
  • NAID: 130005091738
  • Peer Reviewed / Acknowledgement Compliant
• [Journal Article] Design Verification by Model Checking (2014)
  • Author(s): 吉岡信和，田辺良則，田原康之，長谷川哲夫，磯部祥尚
  • Journal Title: Computer Software Volume: 31 Issue: 4 Pages: 4_40-4_65
  • DOI: 10.11309/jssst.31.4_40
  • NAID: 130004892301
  • ISSN: 0289-6540
  • Peer Reviewed
• [Journal Article] Scalaの並行プログラム検査における状態空間探索手法 (2014)
  • Author(s): 島田工，前澤悠太，鄭顕志，田辺良則，本位田真一
  • Journal Title: 第9回ソフトウェアエンジニアリングシンポジウム論文集 Volume: 2014 Pages: 54-59
  • NAID: 170000084817
  • Peer Reviewed
• [Journal Article] Modular Software Model Checking for Distributed Systems (2014)
  • Author(s): Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto, and Koichi Takahashi
  • Journal Title: IEEE Transactions on Software Engineering Volume: - Issue: 5 Pages: 483-501
  • DOI: 10.1109/tse.2013.49
  • Peer Reviewed
• [Journal Article] Software Model Checking for Distributed Systems with Selector-Based, Non-blocking Communication (2013)
  • Author(s): Cyrille Artho, Masami Hagiya, Richard Potter, Yoshinori Tanabe, Franz Weitl, and Mitsuharu Yamamoto
  • Journal Title: 28th IEEE/ACM International Conference on Automated Software Engineering Volume: - Pages: 169-179
  • DOI: 10.1109/ase.2013.6693077
  • Peer Reviewed
• [Journal Article] Modbat: A Model-Based API Tester for Event-Driven Systems (2013)
  • Author(s): Cyrille Valentin Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, and Mitsuharu Yamamoto
  • Journal Title: Proceedings of the 9th Haifa Verification Conference, Lecture Notes in Computer Science Volume: 8244 Pages: 112-128
  • DOI: 10.1007/978-3-319-03077-7_8
  • ISBN: 9783319030760, 9783319030777
  • Peer Reviewed
• [Journal Article] クラウド環境における仮想マシン間通信の最適化に関する検討 (2013)
  • Author(s): 松本敦嗣, 横山重俊
  • Journal Title: 電子情報通信学会技術研究報告 Volume: 113(303) Pages: 1-5
• [Journal Article] アスペクト指向言語を利用したソフトウェアモデル検査手法 (2013)
  • Author(s): 古賀陽一郎，田辺良則
  • Journal Title: ソフトウェア工学の基礎 Volume: 20 Pages: 203-208
  • Peer Reviewed
• [Journal Article] Heuristic Search with Java PathFinder Using Cutoff Policy (2013)
  • Author(s): 前岡 淳, 田辺 良則, 石川 冬樹
  • Journal Title: Computer Software Volume: 30 Issue: 3 Pages: 3_109-3_122
  • DOI: 10.11309/jssst.30.3_109
  • NAID: 130004549315
  • ISSN: 0289-6540
  • Peer Reviewed
• [Journal Article] Implementation of a Memory Disclosure Attack on Memory Deduplication of Virtual Machines (2013)
  • Author(s): K. Suzaki, K. Iijima, T. Yagi, C. Artho
  • Journal Title: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences Volume: E96.A Issue: 1 Pages: 215-224
  • DOI: 10.1587/transfun.E96.A.215
  • NAID: 10031167105
  • ISSN: 0916-8508, 1745-1337
  • Peer Reviewed
• [Journal Article] Computational soundness of indistinguishability properties without computable parsing (2012)
  • Author(s): Hubert Comon-Lundh, Masami Hagiya, Yusuke Kawamoto, and Hideki Sakurada
  • Journal Title: The 8th International Conference on Information Security Practice and Experience (ISPEC 2012), Lecture Notes in Computer Science Volume: 7232 Pages: 63-79
  • DOI: 10.1007/978-3-642-29101-2_5
  • ISBN: 9783642291005, 9783642291012
  • Peer Reviewed
• [Journal Article] Dodai-Deploy: Fast Cluster Deployment Tool (2012)
  • Author(s): Shigetoshi Yokoyama,Nobukazu Yoshioka
  • Journal Title: 19th International Conference on Web Services (ICWS) Volume: - Pages: 681-682
  • DOI: 10.1109/icws.2012.71
  • Peer Reviewed
• [Journal Article] Cluster as a Service for Self-Deployable Cloud Applications (2012)
  • Author(s): Shigetoshi Yokoyama,Nobukazu Yoshioka
  • Journal Title: International Symposium on Cluster, Cloud and Grid Computing, CCGrid 2012 Volume: - Pages: 703-704
  • DOI: 10.1109/ccgrid.2012.64
  • Peer Reviewed
• [Journal Article] 実装コード不具合検出へのJava PathFinder適用に向けた探索範囲削減手法の検討 (2012)
  • Author(s): 前岡淳，田辺良則
  • Journal Title: ソフトウェア工学の基礎 Volume: 19 Pages: 189-194
  • Peer Reviewed
• [Journal Article] Why Do Software Packages Conflict? (2012)
  • Author(s): C. Artho, K. Suzaki, R. di Cosmo, R. Treinen, S. Zacchiroli
  • Journal Title: 9th IEEE Working Conference of Mining Software Repositories Volume: - Pages: 141-150
  • DOI: 10.1109/msr.2012.6224274
  • Peer Reviewed
• [Journal Article] Model checking distributed systems by combining caching and process checkpointing (2011)
  • Author(s): Watcharin Leungwattanakit
  • Journal Title: 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011) Volume: 1 Pages: 103-112
  • DOI: 10.1109/ase.2011.6100043
  • Peer Reviewed
• [Journal Article] Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications (2011)
  • Author(s): Kosuke Ono, Yoichi Hirai, Masami Hagiya Natsuko Noda
  • Journal Title: Lecture Notes in Computer Science Volume: 7041 Pages: 350-365
  • DOI: 10.1007/978-3-642-24690-6_24
  • ISBN: 9783642246890, 9783642246906
  • Peer Reviewed
• [Journal Article] edubase Cloud: An Open-source Cloud Platform for Cloud Engineers (2011)
  • Author(s): Nobukazu Yoshioka, Shigetoshi Yokoyama, Yoshionori Tanabe, Shinichi Honiden
  • Journal Title: SECLOUD '11 Proceedings of the 2nd International Workshop on Software Engineering for Cloud Computing Volume: 1 Pages: 73-73
  • Peer Reviewed
• [Presentation] Precondition Coverage in Software Testing (2016)
  • Author(s): Cyrille Artho, Guillaume Rousset, Quentin Gros
  • Organizer: 1st International Workshop on Validating Software Tests
  • Place of Presentation: 大阪大学 (大阪府大阪市)
  • Year and Date: 2016-03-15
  • Int'l Joint Research
• [Presentation] Classification of Randomly Generated Test Cases (2016)
  • Author(s): Cyrille Artho, Lei Ma
  • Organizer: 1st International Workshop on Validating Software Tests
  • Place of Presentation: 大阪大学 (大阪府大阪市)
  • Year and Date: 2016-03-15
  • Int'l Joint Research
• [Presentation] Domain-Specific Languages with Scala (2015)
  • Author(s): Cyrille Artho, Klaus Havelund, Rahul Kumar, Yoriyuki Yamagata
  • Organizer: 17th International Conference on Formal Engineering Methods
  • Place of Presentation: パリ (フランス)
  • Year and Date: 2015-12-05
  • Int'l Joint Research
• [Presentation] Model-Based Testing of Stateful APIs with Modbat (2015)
  • Author(s): Cyrille Artho, Martina Seidl, Quentin Gros, Eun-Hye Choi, Takashi Kitamura, Akira Mori, Rudolf Ramler, Yoriyuki Yamagata
  • Organizer: 30th IEEE/ACM International Conference on Automated Software Engineering
  • Place of Presentation: リンカーン (米国)
  • Year and Date: 2015-11-13
  • Int'l Joint Research
• [Presentation] GRT: An Automated Test Generator Using Orchestrated Program Analysis (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Johannes Gmeiner, Rudolf Ram\ ler
  • Organizer: 30th IEEE/ACM International Conference on Automated Software Engineering
  • Place of Presentation: リンカーン (米国)
  • Year and Date: 2015-11-12
  • Int'l Joint Research
• [Presentation] GRT: Program-Analysis-Guided Random Testing (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Johannes Gmeiner, Rudolf Ramler
  • Organizer: 30th IEEE/ACM International Conference on Automated Software Engineering
  • Place of Presentation: リンカーン (米国)
  • Year and Date: 2015-11-11
  • Int'l Joint Research
• [Presentation] Cardinality of UDP Transmission Outcomes (2015)
  • Author(s): Franz Weitl, Nazim Sebih, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Mitsuharu Yamamoto
  • Organizer: 1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications
  • Place of Presentation: 南京 (中国)
  • Year and Date: 2015-11-04
  • Int'l Joint Research
• [Presentation] Depth-First Heuristic Search for Software Model Checking (2015)
  • Author(s): Jun Maeoka, Yoshinori Tanabe, Fuyuki Ishikawa
  • Organizer: 14th IEEE/ACIS International Conference on Computer and Information Science
  • Place of Presentation: ラスベガス (米国)
  • Year and Date: 2015-07-01
  • Int'l Joint Research
• [Presentation] GRT at the SBST 2015 Tool Competition (2015)
  • Author(s): Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
  • Organizer: 8th IEEE/ACM International Workshop on Search-Based Software Testing
  • Place of Presentation: フィレンツェ (イタリア)
  • Year and Date: 2015-05-02
  • Int'l Joint Research
• [Presentation] 遷移のキャッシュを行うLTLモデル検査方式 (2015)
  • Author(s): 田辺良則
  • Organizer: 第17回プログラミングおよびプログラミング言語ワークショップ
  • Place of Presentation: 道後プリンスホテル(愛媛県)
  • Year and Date: 2015-03-04 – 2015-03-06
• [Presentation] ソフトウェアモデル検査におけるLTL検証の探索範囲限定手法による効率化 (2014)
  • Author(s): 前岡 淳, 田辺 良則, 石川 冬樹
  • Organizer: 第21回 ソフトウェア工学の基礎ワークショップ
  • Place of Presentation: 霧島国際ホテル (鹿児島県)
  • Year and Date: 2014-12-11 – 2014-12-13
• [Presentation] Software Model Checking of UDP-based Distributed Applications (2014)
  • Author(s): Nazim Sebih, Franz Weitl, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
  • Organizer: The Second International Symposium on Computing and Networking (CANDAR 2014)
  • Place of Presentation: 静岡県コンベンションアーツセンター (静岡県)
  • Year and Date: 2014-12-10 – 2014-12-12
• [Presentation] Using Checkpointing and Virtualization for Fault Injection (2014)
  • Author(s): Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Eric Platon, Richard Potter, Kuniyasu Suzaki, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
  • Organizer: The Second International Symposium on Computing and Networking (CANDAR 2014)
  • Place of Presentation: 静岡県コンベンションアーツセンター (静岡県)
  • Year and Date: 2014-12-10 – 2014-12-12
• [Presentation] Model-based testing (2014)
  • Author(s): Cyrille Artho
  • Organizer: Shonan Meeting 2014-16
  • Place of Presentation: 湘南国際村センター (神奈川県)
  • Year and Date: 2014-12-01 – 2014-12-04
• [Presentation] Scalaの並行プログラム検査における状態空間探索手法 (2014)
  • Author(s): 島田工，前澤悠太，鄭顕志，田辺良則，本位田真一
  • Organizer: 第9回ソフトウェアエンジニアリングシンポジウム
  • Place of Presentation: 芝浦工業大学 (東京都)
  • Year and Date: 2014-09-01 – 2014-09-03
• [Presentation] Network traffic optimization architecture for scalability in academic inter-cloud computing environments (2014)
  • Author(s): Shigetoshi Yokoyama, Atsushi Matsumoto and Nobukazu Yoshioka
  • Organizer: International Workshop on Hot Topics in Cloud service Scalability
  • Place of Presentation: Clyde Court Hotel, Dublin (アイルランド)
• [Presentation] Software Model Checking for Distributed Systems with Selector-Based, Non-Blocking Communication (2013)
  • Author(s): C. Artho, M. Hagiya, R. Potter, Y. Tanabe, F. Weitl, M. Yamamoto
  • Organizer: 28th Int. Conf. on Automated Software Engineering
  • Place of Presentation: Crowne Plaza Cabana（米国、カリフォルニア州）
• [Presentation] Modbat: A Model-based API Tester for Event-driven Systems (2013)
  • Author(s): C. Artho, A. Biere, M. Hagiya, M. Seidl, E. Platon, Y. Tanabe, M. Yamamoto
  • Organizer: 9th Haifa Verification Conference
  • Place of Presentation: IBM Research（イスラエル、Haifa）
• [Presentation] The Quest for Precision: A Layered Approach for Data Race Detection in Static Analysis (2013)
  • Author(s): J. Mund, R. Huuck, A. Fehnker, C. Artho
  • Organizer: 11th Int. Symposium on Automated Technology for Verification and Analysis
  • Place of Presentation: ベトナム国立大学（ベトナム、ハノイ）
• [Presentation] Analyzing Multi-process Java Program by Automatic Centralization (2013)
  • Author(s): L. Ma, C. Artho, H. Sato
  • Organizer: 2nd IEEE Int. Workshop on Tools in Process
  • Place of Presentation: 京都テルサ（京都）
• [Presentation] Model-based Testing for Verification Backends (2013)
  • Author(s): A. Biere, M. Seidl, C. Artho
  • Organizer: Tests and Proofs (TAP) 2013
  • Place of Presentation: ブダペスト（ハンガリー）
• [Presentation] With an Open Mind: How to Write Good Models (2013)
  • Author(s): C. Artho, K. Hayamizu, R. Ramler, Y. Yamagata
  • Organizer: 2nd Int. Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2013)
  • Place of Presentation: Crowne Plaza Hotel, Queenstown (ニュージーランド)
• [Presentation] Java PathFinderを使用したOpenFlowコントローラのモデル検査 (2013)
  • Author(s): 穂浪勇利，田辺良則，萩谷昌己
  • Organizer: 第30回 日本ソフトウェア科学会大会
  • Place of Presentation: 東京大学 (東京都)
• [Presentation] アスペクト指向言語を利用したソフトウェアモデル検査手法 (2013)
  • Author(s): 古賀陽一郎，田辺良則
  • Organizer: 第20回 ソフトウェア工学の基礎ワークショップ (FOSE 2013)
  • Place of Presentation: ゆのくに天祥 (石川県)
• [Presentation] フィールドアクセスに着目したモデル検査の効率化 (2013)
  • Author(s): 前岡 淳, 田辺 良則, 石川 冬樹
  • Organizer: 第20回 ソフトウェア工学の基礎ワークショップ (FOSE 2013)
  • Place of Presentation: ゆのくに天祥 (石川県)
• [Presentation] Modbat: A model-based API tester for event-driven systems (2012)
  • Author(s): C. Artho, A. Biere, M. Hagiya, R. Potter, R. Ramler, Y. Tanabe, F. Weitl, M. Yamamoto
  • Organizer: the Dependable Systems Workshop 2012
  • Place of Presentation: 計算科学研究機構（兵庫）
• [Presentation] Why Do Software Packages Conflict? (2012)
  • Author(s): C. Artho, K. Suzaki, R. di Cosmo, R. Treinen, S. Zacchiroli
  • Organizer: 9th Working Conference on Mining Software Repositories
  • Place of Presentation: チューリッヒ（スイス）
• [Presentation] Effects of Memory Randomization, Sanitization and Page Cache on Memory Deduplication (2012)
  • Author(s): K. Suzaki, K. Iijima, T. Yagi, C. Artho
  • Organizer: 5th European Workshop on System Security
  • Place of Presentation: ベルン（スイス）
• [Presentation] Dodai-Deploy: Fast Cluster Deployment Tool (2012)
  • Author(s): Shigetoshi Yokoyama,Nobukazu Yoshioka
  • Organizer: 19th International Conference on Web Services (ICWS)
  • Place of Presentation: ハワイ（米国）
• [Presentation] Cluster as a Service for Self-Deployable Cloud Applications (2012)
  • Author(s): Shigetoshi Yokoyama,Nobukazu Yoshioka
  • Organizer: International Symposium on Cluster, Cloud and Grid Computing, CCGrid 2012
  • Place of Presentation: Ottawa(カナダ)
• [Presentation] 実装コード不具合検出へのJava PathFinder適用に向けた探索範囲削減手法の検討 (2012)
  • Author(s): 前岡淳，田辺良則
  • Organizer: 第19回 ソフトウェア工学の基礎ワークショップ (FOSE 2012)
  • Place of Presentation: ゆふいん山水館 (大分)
• [Presentation] AOPを応用した実用的なソースコードモデル検査手法 (2012)
  • Author(s): 古賀 陽一郎，田辺 良則
  • Organizer: 第178回情報処理学会ソフトウェア工学研究発表会
  • Place of Presentation: 広島市立大学 (広島)
• [Presentation] Model Checking Distributed Systems by Combining Caching and Process Checkpointing (2011)
  • Author(s): W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto
  • Organizer: 26th Int. Conf. on Automated Software Engineering (ASE 2011)
  • Place of Presentation: Oread, Lawrence, Kan, USA
• [Presentation] Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications (2011)
  • Author(s): Kosuke Ono, Yoichi Hirai, Yoshinori Tanabe, Natsuko Noda, Masami Hagiya
  • Organizer: 9th International Conference of Software Engineering and Formal Methods, SEFM 2011
  • Place of Presentation: Montevideo, Uruguay
• [Presentation] ネットワークアプリケーションのマスター・スレーブ方式モデル検査アルゴリズムについて (2011)
  • Author(s): 田辺 良則, Cyriile Artho, Watcharin Leungwattanakit, 山本 光晴, 萩谷 昌己
  • Organizer: 日本ソフトウェア科学会第28回大会
  • Place of Presentation: 沖縄産業支援センター，沖縄県那覇市
• [Presentation] edubase Cloud: An Open-source Cloud Platform for Cloud Engineers
  • Author(s): Nobukazu Yoshioka, Shigetoshi Yokoyama, Yoshionori Tanabe, Shinichi Honiden
  • Organizer: 2nd International Workshop on Software Engineering for Cloud Computing
  • Place of Presentation: Waikiki, Honolulu, Hawaii, USA
• [Presentation] Analysis of networked software
  • Author(s): Cyrille Artho
  • Organizer: 第4回新世代ネットワークおよび将来インターネットに関する日欧シンポジウム
  • Place of Presentation: TKP東京駅八重洲カンファレンスセンター (東京都)
• [Presentation] Analysis of networked and cloud computing software
  • Author(s): Cyrille Artho
  • Organizer: International Workshop on Embedded Security of System and Software (IWESSS'12)
  • Place of Presentation: National University of Singapore (シンガポール)
• [Presentation] Analysis of networked and cloud computing software
  • Author(s): Cyrille Artho
  • Organizer: 第2回ソフトウェアと検証のワークショップ
  • Place of Presentation: 産業技術総合研究所 (兵庫県)