A novel approach to verifying context free properties of programs.

This paper proposes an approach to verifying context free properties of programs. In this approach, the system to be verified is modeled as a program m in Modeling, Simulation and Verification Language (MSVL), and the desired property is also specified by an MSVL program m′. Then program m and formula ¬m′ are interpreted by means of executing programs m and m′. If an acceptable execution path is generated, a counterexample is found, otherwise the property is valid. To show how the proposed approach works, an example is given.