Development of formally verifiable framework for program transformation
| Project/Area Number |
20500011
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2008 – 2011
|
| Project Status |
Completed (Fiscal Year 2011)
|
| Budget Amount *help |
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2011: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2010: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2009: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2008: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| Keywords | プログラム理論 / プログラム変換 / 形式的証明 / 形式的検証 / 並行プログラム |
|---|
| Research Abstract |
We have developed a method, which is an extension of the stepwise refinement method, for correctness-preserving transformation of programs that make use of advanced features such as pointer manipulations and exceptions. We have shown that each feature has a corresponding logical system, namely, separation logic for pointer manipulations and four-valued logic for exceptions. It has been shown that the correctness of programs is formally guaranteed by developing formal proofs on computers, based on each particular logical system.
|
Report
(6 results)
Research Products
(24 results)
