| Budget Amount *help |
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2014: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2013: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2012: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Outline of Final Research Achievements |
Modeling and verification of various systems are expected to be important applications of non-procedural high-level languages. The Principal Investigator has long worked on the design and implementation of a modeling language based on graph rewriting that supports ordinary execution and model checking in a unified framework, but the evolution and verification of its compiler has been recognized as a challenging issue. In this study, we formalized and verified graph rewriting operations performed by the abstract machine that is the interface between the compiler and the runtime, and made a step towards the verification of a graph rewriting compiler. Also, we established novel type systems for the graph rewriting language that will help the analysis, understanding and compiler optimization of models. One of them handles microscopic connectivity of graphs and hypergraphs, while the other handles the global shape of graphs.
|
