On constructing a tool to verify programs for processors built in machines

The paper proposes a method of constructing a tool which is used to verify programs in embedded processors by using our framework of program understanding, which is based on the world model. Though a lot of tools for software development are proposed, it seems that they can´t be applied to our target programs. So we need a new framework to approach our goal. We think that the point is how to deal with constraints by individual hardware, including mechanics. We have been studying a framework for program understanding based on the world model. Thus, we discuss a way to apply program understanding to verification of software. We discuss the following: the structure of the world model; outline of program understanding; how to describe the result of understanding and specifications; how to match them; and how to display the result of matching. We introduce a prototype system and show the experimental results to evaluate our framework