| Budget Amount *help |
¥3,740,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥240,000)
Fiscal Year 2007: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2006: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 2005: ¥1,400,000 (Direct Cost: ¥1,400,000)
|
|---|
| Research Abstract |
The objective of this research is to apply the theory of "Verifying Compilers" to compiler optimization, and to investigate the mathematical theory of compiler optimizations, and to broaden the area of verifications. The concept of verifying compilers is originally proposed by CAR Hoare. Today, compiler optimization have become complicated, and error-prone because of their complexities. In this research, we aim at building a compiler system in which an application of an optimization is automatically verified, and the correctness of the generated codes is also automatically guaranteed.
This year, we studied the extraction of knowledge of optimizations in a Web community, which has rapidly emerged as a computing platform. Concretely, we have succeeded in extracting knowledge related to programming. We have seen that the result is intuitively correct. Furthermore, we have revealed that the formalization of computing in a distributed environment is closely related to security description, which is a neighbor to correctness guarantee. Concretely, we have proposed a method of formalizing a business workflow, and of representing it in a document.
Moreover, we have studied "performance tuning beyond compiler optimizations," in which we have broaden the search space of candidates of optimizations. Concretely we have applied higher order program transformations to numerical programs, and have found the wider space of candidate search.
|
