| 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.
|
