US Patent 7783470 Verification of concurrent programs having parameterized qualities

A system and method for computing dataflow in concurrent programs of a computer system, like device drivers which control computer hardware like disk drives, audio speakers, etc., includes, given a concurrent program that includes many similar components, initializing a set of reachable control states for interaction between concurrent programs. Based on the set of reachable control states, synchronization constructs are removed between the control states. The synchronization constructs are replaced with internal transitions. New reachable control states uncovered by the removal of the synchronization constructs are added where the new reachable control states are discovered using model checking for single threads. Data race freedom of the plurality of concurrent programs is verified by reviewing a complete set of reachable control states.