1. A method for computing dataflow in concurrent programs of a computer system, comprising: given a family of threads (U 1 ,. .. , U m ) and a Linear Temporal Logic (LTL) property, f, for a concurrent program, computing a cutoff for the LTL property, f, where c is called the cutoff if for all n greater than or equal to c, U n satisfies f if U c satisfies f, the cutoff being computed using weighted multi-automata for internal transitions of the threads; and model checking a cutoff number of processes to verify race freedom in the concurrent program.