partitioning a state space of a circuit under analysis into a plurality of partitions, the plurality of partitions comprising one or more first partitions and one or more second partitions;

assigning each of the plurality of partitions to a thread to carry out a reachability analysis on the partition assigned to the thread, the threads carrying out the reachability analyses of the plurality of partitions in parallel with each other using a computer; and

using one or more of an early communication algorithm or a partial communication algorithm to communicate states from one or more of the first partitions to one or more of the second partitions to facilitate the reachability analysis of the one or more of the second partitions;

wherein, according to the early communication algorithm:

a first partition communicates one or more of its reached states to a second partition after the first partition has reached a least fixed point, the second partition not having reached a least fixed point when the first partition communicates the reached states; and

in response to the communication of the reached states, the second partition incorporates the communicated states and a current image computation restarts in the second partition to augment the reachability analysis in the second partition.