Evolutionary development of a model checker compiler using verification technology and non-standard type systems

2014 Fiscal Year Final Research Report

• Project/Area Number: 24650016
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: Waseda University
• Principal Investigator: UEDA Kazunori 早稲田大学, 理工学術院, 教授 (10257206)
• Project Period (FY): 2012-04-01 – 2015-03-31
• Keywords: モデル検査 / コンパイラ / 検証 / 型体系 / ソフトウェア進化

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.

Free Research Field

プログラミング言語