SYNTHESIS OF VERIFICATION LANGUAGES

摘要

A method for synthesizing a verification language, and thereby enabling the verification language to be compiled into a target language. This method enables the underlying control structure of the verification language to be determined, and then used to map the dynamic behavior of the verification language onto the target language as part of a static framework. The process of synthesizing any type of verification language causes at least a portion of the implicit control structure of the software program to be constructed into the compiled output code, such that an additional scheduler or other type of runtime system may not be required. Therefore, the compiled output code should have a greater execution speed and should be operated more efficiently than the software programs which are written in the verification language itself.