#x03BC;-calculus of process trees with their application

摘要

To solve the problems of structure abstract representation in the software verification process, we define method of using process tree represent program, which can better represent program sequence structure and the relationship between call and return. Based on this data structures and μ-calculus, we definite μ - calculus of the process tree (PT − μ). Representation is divided into two levels: the first level take the nodes in a process tree as the basic unit, the second level take the summary as the basic unit. Summary is based on the relationship between call and return to represent the process of implementation, which also consider the possible simultaneous execution of other processes. PT − μ formulas also take into account of the classification of executive relations in the program. Experiments show that PT − μ can better represent the needs that to be verified, and better represent the reachability properties and better reflect the data flow relations in the data flow analysis.