Type Inference of Object-Oriented Programs with Exceptions Based on Term Rewriting

2007 Fiscal Year Final Research Report Summary

• Project/Area Number: 16300005
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Nagoya University
• Principal Investigator: SAKABE Toshiki Nagoya University, School of Information Science, Professor (60111829)
• Co-Investigator(Kenkyū-buntansha): SAKAI Masahiko Nagoya University, School of Information Science, Professor (50215597) ; KUSAKARI Keiichirou Nagoya University, School of Information Science, Associate Professor (90323112) ; NISHIDA Naoki Nagoya University, School of Information Science, Assistant Professor (00397449)
• Project Period (FY): 2004 – 2007
• Keywords: Object-Oriented Program / Exception Handling / Secrecy / Type Inference / Term Rewriting System

Research Abstract

The purpose of this research is to develop static verification methods for safeness of programs by applying rich results obtained so far on term rewriting systems, and also to create new research topics of term rewriting systems.
There are three main topics of this research : safeness of programs, termination of term rewriting systems and program transformations. (1) As for safeness of programs, we have developed a type system for verifying secrecy of object-oriented programs with exceptions, a type system for checking communication errors in programs of Join JAVA, which is a JAVA combined with Join Calculus, and also methods for verifying safeness of programs of Spi Calculus and Petri Net. (2) For termination of term rewriting systems, a result on decidability of termination has been obtained. Sufficient conditions for termination of higher order term rewriting systems have been obtained by extending the dependency pair method. (3) In the research of program transformation, an inversion procedure for term rewriting systems has been developed. Being triggered by the work on program safeness we have given a sufficient condition for termination of a procedure transforming systems of eqations to systems of rewriting rules, where this transformation is used in the secrecy verification procedure for the applied pi calculus.

Research Products

• [Journal Article] 例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム (2008)
  • Author(s): 黒川翔, 桑原寛明, 山本晋一郎, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹
  • Journal Title: 電子情報通信学会論文誌 J91-D Pages: 757-770
  • Description: 「研究成果報告書概要(和文)」より
  • Peer Reviewed
• [Journal Article] Error Detection with Soft Typing for Dynamically Typed Language (2008)
  • Author(s): Akihisa Yamada, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe and Naoki Nishida
  • Journal Title: IEICE Technical Report SS2007-58 107 Pages: 7-12
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques (2008)
  • Author(s): Keiichirou Kusakari, Masahiko Sakai
  • Journal Title: IEICE Technical Report SS2007-60 107 Pages: 19-24
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] 等式を規則化する変換の停止条件 (2008)
  • Author(s): 水野清貴, 西田直樹, 坂部俊樹、酒井正彦, 草刈圭一朗
  • Journal Title: 電子情報通信学会技術研究報告(SS2007-61) 107 Pages: 25-30
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] A Type System for Analyzing Secure Information Flow in Object-Oriented Programs with Exception Handling (2008)
  • Author(s): Sho, Kurokawa, Hiroaki, Kuwabara, Shin-ichiro, Yamamoto, Toshiki, Sakabe, Masahiko, Sakai, Keiichirou, Kusakari, Naoki, Nishida
  • Journal Title: IEICE Transactions on Information and Systems Vol.J91-D, No.3(Refereed) Pages: 757-770
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Error Detection with Soft Typing for Dynamically Typed Language (2008)
  • Author(s): Akihisa, Yamada, Keiichirou, Kusakari, Masahiko, Sakai, Toshiki, Sakabe, Naoki, Nishida
  • Journal Title: IEICE Technical Report SS2007-58 Vol.107, No.505(Non-refereed) Pages: 7-12
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques (2008)
  • Author(s): Keiichirou, Kusakari, Masahiko, Sakai
  • Journal Title: IEICE Technical Report SS2007-60 107(Non-refereed) Pages: 19-24
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] A Sufficient Condition for Termination of Transforma-tions from Equations to Rewrite Rules (2008)
  • Author(s): Kiyotaka, Mizuno, Naoki, Nishida, Toshiki, Sakabe, Masahiko, Sakai, Keiichirou, Kusakari
  • Journal Title: IEICE Technical Report (SS2007-6) Vol.107, No.505(Non-refereed) Pages: 25-30
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Enhancing Dependency Pair Method by Strong Computability in Simply-Typed Term Rewriting (2007)
  • Author(s): Keiichirou Kusakari, Masahiko Sakai
  • Journal Title: Applicable Algebra in Engineering, Communica-tion and Computing 18 Pages: 407-431
  • Description: 「研究成果報告書概要(和文)」より
  • Peer Reviewed
• [Journal Article] 単純型項書き換え系上の依存対法における実効規則と直積型項へのラベル付け (2007)
  • Author(s): 櫻井敬大、草刈圭一朗、酒井正彦、坂部俊樹、西田直樹
  • Journal Title: 電子情報通信学会論文誌 J90-D Pages: 978-989
  • Description: 「研究成果報告書概要(和文)」より
  • Peer Reviewed
• [Journal Article] Decidability of Innermost Termination and Context-Sensitive Termina-tion for Semi-Constructor Term Rewriting Systems (2007)
  • Author(s): Keita Uchiyama, Masahiko Sakai and Toshiki Sakabe
  • Journal Title: Proc. of 7th International Workshop on Reduc-tion Strategies in Rewriting and Programming Pages: 16-27
  • Description: 「研究成果報告書概要(和文)」より
  • Peer Reviewed
• [Journal Article] Convergent Term Rewriting Systems for Inverse Computation of Injec-tive Fhnctions (2007)
  • Author(s): Naoki Nishida, Masahiko Sakai, and Terutoshi Kato
  • Journal Title: Proc. of the 9th International Workshop on Ter-mination Pages: 77-81
  • Description: 「研究成果報告書概要(和文)」より
  • Peer Reviewed
• [Journal Article] Static Dependency Pair Method for Proving Termination of Higher-Order Rewriting Systems (2007)
  • Author(s): Kiichirou Kusakari, Yasuo Iso-gai, Masahiko Sakai, Toshiki Sakabe Naoki Nishida
  • Journal Title: 電子情報通信学会技術研究報告(SS2007-61) 107 Pages: 17-22
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] 左線形は定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン (2007)
  • Author(s): 村田俊樹、西田直樹、酒井正彦、坂部俊樹、草刈圭一朗
  • Journal Title: 電子情報通信学会技術研究報告(SS2007-61) 107 Pages: 1-6
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] 振舞等価性の証明のための等式付き書換えに基づく潜在帰納法 (2007)
  • Author(s): 笹田悠司、酒井正彦、西田直樹、坂部俊樹、草刈圭一朗
  • Journal Title: 電子情報通信学会技術研究報告(SS2007-61) 107 Pages: 7-12
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] Enhancing Dependency Pair Method by Strong Com-putability in Simply-Typed Term Rewriting (2007)
  • Author(s): Keiichirou, Kusakari, Masahiko, Sakai
  • Journal Title: Applicable Algebra in Engineering, Communica-tion and Computing Vol.18, No.5(Refereed) Pages: 407-431
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Usable Rules and Labeling Product-Typed Terms for De-pendency Pair Method in Simply-Typed Term Rewriting Systems (2007)
  • Author(s): Takahiro, Sakurai, Keiichirou, Kusakari, Masahiko, Sakai, Toshiki, Sakabe, Naoki, Nishida
  • Journal Title: IEICE Transactions on Information and Systems Vol.J90-D, No.4(Refereed) Pages: 978-989
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems (2007)
  • Author(s): Keita, Uchiyama, Masahiko, Sakai, Toshiki, Sakabe
  • Journal Title: Proc. of 7th International Workshop on Reduc-tion Strategies in Rewriting and Programming (Refereed) Pages: 16-27
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Convergent Term Rewriting Systems for Inverse Compu-tation of Injective Functions (2007)
  • Author(s): Naoki, Nishida, Masahiko, Sakai, Terutoshi, Kato
  • Journal Title: Proc. of the 9th International Workshop on Ter-mination (Refereed) Pages: 77-81
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Static Dependency Pair Method for Proving Termination of Higher-Order Rewriting Systems (2007)
  • Author(s): Keichirou, Kusakari, Yasuo, Isogai, Masahiko, Sakai, Toshiki, Sakabe Naoki, Nishida
  • Journal Title: IEICE Technical Report (SS2007-61) Vol.107, No.505(Non-refereed) Pages: 17-22
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Recognizable Approximation of Descendant Sets for Left-Linear Oriented Conditional Term Rewriting Systems (2007)
  • Author(s): Toshiki, Murata, Naoki, Nishida, Masahiko, Sakai, Toshiki, Sakabe, Keiichirou, Kusakari
  • Journal Title: IEICE Technical Report (SS2007-16) Vol.107, No.176(Non-refereed) Pages: 1-6
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Implicit Induction for Proving Behavioral Equivalence by Equational Rewriting (2007)
  • Author(s): Yuji, Sasada, Masahiko, Sakai, Naoki, Nishida, Toshiki, Sakabe, Keiichirou, Kusakari
  • Journal Title: IEICE Technical Report (SS2007-17) Vol.107, No.176(Non-refereed) Pages: 7-12
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み (2006)
  • Author(s): 古市祐樹, 西田 直樹, 酒井 正彦, 草刈 圭一朗, 坂部 俊樹
  • Journal Title: 電子情報通信学会技術研究報告(SS2006-41) 106 Pages: 7-12
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] 例外処理付きオブジェクト指向言語における情報流の安全性解析 (2006)
  • Author(s): 黒川 翔, 桑原寛明, 山本晋一郎, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹
  • Journal Title: 電子情報通信学会技術研究報告(SS2006-42) 106 Pages: 13-18
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] 等式付き書換え系の等式数を削減する変換 (2006)
  • Author(s): 三浦浩一, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗
  • Journal Title: 電子情報通信学会技術研究報告(SS2006-14) 106 Pages: 7-12
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] Transformation for Refining Unraveled Conditional Term Rewriting Sys-tems (2006)
  • Author(s): Naoki Nishida, Tomohiro Mizu-tarsi, and Masahiko Sakai
  • Journal Title: Proc. of 6th International Workshop on Reduc-tion Strategies in Rewriting and Programming(WRS2006) Pages: 34-48
  • Description: 「研究成果報告書概要(和文)」より
  • Peer Reviewed
• [Journal Article] 項正規表現に基づくSpi計算の機密性検証 (2006)
  • Author(s): 田代善彦, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹
  • Journal Title: 電子情報通信学会技術研究報告(SS2005-82) 105 Pages: 35-40
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] 関数プログラムの停止性証明に関する辞書式経路順序 (2006)
  • Author(s): 星野由美, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹
  • Journal Title: 電子情報通信学会技術研究報告(SS2005-82) 105 Pages: 35-40
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] Approach to Software Verification Based on Transform-ing from Procedural Programs to Rewrite Systems (2006)
  • Author(s): Yuki, Furuichi, Naoki, Nishida, Masahiko, Sakai, Keiichi-rou, Kusakari, Toshiki, Sakabe
  • Journal Title: IEICE Technical Report (SS2006-41) Vol.106, No.324(No-refereed) Pages: 7-12
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Security Analysis of Information Flow for an Object-Oriented Language with Exception Handling (2006)
  • Author(s): Sho, Kurokawa, Hiroaki, Kuwabara, Shin-ichiro, Yamamoto, Toshiki, Sakabe, Masahiko, Sakai, Keiichirou, Kusakari, Naoki, Nishida
  • Journal Title: IEICE Technical Report (SS2006-42) Vol.106, No.324(Non-refereed) Pages: 13-18
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Transformation of Equational Rewriting Systems for Re-moving Some Equations (2006)
  • Author(s): Kiochi, Miura, Naoki, Nishida, Masahiko, Sakai, Toshiki, Sakabe, Keiichirou, Kusakari
  • Journal Title: IEICE Technical Report (SS2006-14) Vol.106, No.120(Non-refereed) Pages: 7-12
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Transformation for Refining Unraveled Conditional Term Rewriting Systems (2006)
  • Author(s): Naoki, Nishida, Tomohiro, Mizutani, Masahiko, Sakai
  • Journal Title: Proc. of 6th International Workshop on Reduc-tion Strategies in Rewriting and Programming (WRS2006) (Refereed) Pages: 34-48
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Secrecy Verification of Spi Calculus based on Term Reg-ular Expressions (2006)
  • Author(s): Yoshihiko, Tashiro, Toshiki, Sakabe, Masahiko, Sakai, Keiichirou, Kusakari, Naoki, Nishida
  • Journal Title: IEICE Technical Report IEICE (SS2005-82) Vol.105, No.596(Non-refereed) Pages: 35-40
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Lexicographic Path Ordering for Proving Termination of Functional Programs (2006)
  • Author(s): Yumi, Hoshino, Keiichirou, Kusakari, Masahiko, Sakai, Toshiki, Sakabe, Naoki, Nishida
  • Journal Title: IEICE Technical Report (SS2005-85) Vol.105, No.596(Non-refereed) Pages: 35-40
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] 分散JoinJAVAプログラムの通信エラーに対する型判定システム (2005)
  • Author(s): 佐伯昌樹, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹
  • Journal Title: 電子情報通信学会技術研究報告(SS2005-67) 105 Pages: 25-30
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] 暗号プロトコル記述からカラーペトリネットへの変換による機密性検証 (2005)
  • Author(s): 奥谷大介, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹
  • Journal Title: 電子情報通信学会技術研究報告(SS2005-58) 105 Pages: 19-24
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] 重なりを持つTRSにおける最外戦略の完全性について (2005)
  • Author(s): 岩田篤史, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹
  • Journal Title: 電子情報通信学会技術報告(SS2005-46) 105 Pages: 39-44
  • Description: 「研究成果報告書概要(和文)」より
• [Journal Article] Type Judgement System for Communication Error in Distributed Join JAVA Programs (2005)
  • Author(s): Saeki, Masaki, Toshiki, Sakabe, Masahiko, Sakai, Keiichirou, Kusakari, Naoki, Nishida
  • Journal Title: IEICE Technical Report (SS2005-67) Vol.105, No.491(Non-refereed) Pages: 25-30
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] Secrecy Verification by Transforming Cryptographic Pro-tocol Descripstions to Coloured Petri Nets (2005)
  • Author(s): Okuya, Daisuke, Toshiki, Sakabe, Masahiko, Sakai, Keiichirou, Kusakari, Naoki, Nishida
  • Journal Title: IEICE Technical Report (SS2005-58) Vol.105, No.490(Non-refereed) Pages: 19-24
  • Description: 「研究成果報告書概要(欧文)」より
• [Journal Article] On Completeness of Outermost Strategy for Overlapping TRSs (2005)
  • Author(s): Atsushi, Iwata, Masahiko, Sakai, Naoki, Nishida, Keiichirou, Kusakari, Toshiki, Sakabe
  • Journal Title: IEICE Technical Report (SS2005-46) Vol.105, No.331(Non-refereed) Pages: 39-44
  • Description: 「研究成果報告書概要(欧文)」より