Approach of concurrent object-oriented program slicing based on LTL property
一种基于LTL性质的面向对象并发程序切片方法

An approach for slicing concurrent object-oriented programs is presented to reduce the state space in the process of program verification. The dependencies between statements in the given program are defined, and the method of extracting the slicing criterion from linear temporal logic property is introduced. The satisfaction of the verified LTL property is guaranteed for both programs before and after slicing, and the number of states in the state transition graph is decreased.