  Nondeterminism in scheduling is the cardinal reason for difficulty in proving
correctness of concurrent programs. A powerful proof strategy was recently
proposed [6] to show the correctness of such programs. The approach captured
data-flow dependencies among the instructions of an interleaved and error-free
execution of threads. These data-flow dependencies were represented by an
inductive data-flow graph (iDFG), which, in a nutshell, denotes a set of
executions of the concurrent program that gave rise to the discovered data-flow
dependencies. The iDFGs were further transformed in to alternative finite
automatons (AFAs) in order to utilize efficient automata-theoretic tools to
solve the problem. In this paper, we give a novel and efficient algorithm to
directly construct AFAs that capture the data-flow dependencies in a concurrent
program execution. We implemented the algorithm in a tool called ProofTraPar to
prove the correctness of finite state cyclic programs under the sequentially
consistent memory model. Our results are encouranging and compare favorably to
existing state-of-the-art tools.
