Type Inference of Object-Oriented Programs with Exceptions Based on Term Rewriting
| 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
|
| Project Status |
Completed (Fiscal Year 2007)
|
| Budget Amount *help |
¥6,030,000 (Direct Cost: ¥5,700,000、Indirect Cost: ¥330,000)
Fiscal Year 2007: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2006: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2005: ¥1,200,000 (Direct Cost: ¥1,200,000)
Fiscal Year 2004: ¥2,500,000 (Direct Cost: ¥2,500,000)
|
|---|
| 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.
|
Report
(5 results)
Research Products
(61 results)
-
-
-
-
-
[Journal Article] A Type System for Analyzing Secure Information Flow in Object-Oriented Programs with Exception Handling2008
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
NAID
Description
「研究成果報告書概要(欧文)」より
Related Report
-
[Journal Article] Error Detection with Soft Typing for Dynamically Typed Language2008
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
NAID
Description
「研究成果報告書概要(欧文)」より
Related Report
-
-
[Journal Article] A Sufficient Condition for Termination of Transforma-tions from Equations to Rewrite Rules2008
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
「研究成果報告書概要(欧文)」より
Related Report
-
-
-
-
-
-
-
-
-
[Journal Article] Usable Rules and Labeling Product-Typed Terms for De-pendency Pair Method in Simply-Typed Term Rewriting Systems2007
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
「研究成果報告書概要(欧文)」より
Related Report
-
-
-
-
[Journal Article] Recognizable Approximation of Descendant Sets for Left-Linear Oriented Conditional Term Rewriting Systems2007
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
NAID
Description
「研究成果報告書概要(欧文)」より
Related Report
-
[Journal Article] Implicit Induction for Proving Behavioral Equivalence by Equational Rewriting2007
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
NAID
Description
「研究成果報告書概要(欧文)」より
Related Report
-
-
-
-
-
-
-
-
-
-
-
[Journal Article] Approach to Software Verification Based on Transform-ing from Procedural Programs to Rewrite Systems2006
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
「研究成果報告書概要(欧文)」より
Related Report
-
[Journal Article] Security Analysis of Information Flow for an Object-Oriented Language with Exception Handling2006
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
NAID
Description
「研究成果報告書概要(欧文)」より
Related Report
-
[Journal Article] Transformation of Equational Rewriting Systems for Re-moving Some Equations2006
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
「研究成果報告書概要(欧文)」より
Related Report
-
-
[Journal Article] Secrecy Verification of Spi Calculus based on Term Reg-ular Expressions2006
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
NAID
Description
「研究成果報告書概要(欧文)」より
Related Report
-
[Journal Article] Lexicographic Path Ordering for Proving Termination of Functional Programs2006
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
NAID
Description
「研究成果報告書概要(欧文)」より
Related Report
-
-
-
-
-
-
-
-
-
-
-
-
[Journal Article] Type Judgement System for Communication Error in Distributed Join JAVA Programs2005
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
NAID
Description
「研究成果報告書概要(欧文)」より
Related Report
-
[Journal Article] Secrecy Verification by Transforming Cryptographic Pro-tocol Descripstions to Coloured Petri Nets2005
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
「研究成果報告書概要(欧文)」より
Related Report
-
[Journal Article] On Completeness of Outermost Strategy for Overlapping TRSs2005
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
NAID
Description
「研究成果報告書概要(欧文)」より
Related Report
-
-
-
-
-
-
-
-
-
