A method of automatically creating a plurality of output test vectors from a statechart in a verification of software, wherein the statechart specifies requirements of a system function to be executed by a system-performing device and comprises a plurality of states including an initial state (210, 236) and a final state, a plurality of variables and a plurality of transitions (222, 224, 226, 232, 262, 320, 272, 322, 324), wherein at least one transition of the plurality of transitions comprises a condition expressed in terms of at least one variable in the plurality of variables, comprising: providing a processor, and data storage having machine-language instructions executable by the processor to perform a method comprising: generating a plurality of forward-reached-transition environments using a forward-propagation pass (640, 700) through the statechart, wherein each forward-reached-transition environment in the plurality of forward-reached-transition environments is generated for a forward-reached transition forward propagated during the forward-propagation pass; determining a transition was unreached during the forward-propagation pass; responsive to the determination that a transition was unreached during the forward-propagation pass, generating (660, 860) a plurality of backward-reached-transition environments via a backward-propagation pass through the statechart, wherein each backward-reached-transition environment in the plurality of backward-reached-transition environments is generated for a backward-reached transition propagated during the backward-propagation pass; determining a transition was unreached during both the forward-propagation pass and the backward-propagation pass; responsive to the determination that a transition was unreached during both the forward-propagation pass and the backward-propagation pass, performing alternating passes of forward-propagation and backwards-propagation until a sufficient number of transitions has been reached by a pass of forward-propagation and backward-propagation; generating (690, 910) a plurality of output test vectors from the plurality of forward-reached-transition environments and the plurality of backward-reached-transition environments; outputting the plurality of output test vectors; and verifying the software using the output test vectors. generating a plurality of forward-reached-transition environments using a forward-propagation pass (640, 700) through the statechart, wherein each forward-reached-transition environment in the plurality of forward-reached-transition environments is generated for a forward-reached transition forward propagated during the forward-propagation pass; determining a transition was unreached during the forward-propagation pass; responsive to the determination that a transition was unreached during the forward-propagation pass, generating (660, 860) a plurality of backward-reached-transition environments via a backward-propagation pass through the statechart, wherein each backward-reached-transition environment in the plurality of backward-reached-transition environments is generated for a backward-reached transition propagated during the backward-propagation pass; determining a transition was unreached during both the forward-propagation pass and the backward-propagation pass; responsive to the determination that a transition was unreached during both the forward-propagation pass and the backward-propagation pass, performing alternating passes of forward-propagation and backwards-propagation until a sufficient number of transitions has been reached by a pass of forward-propagation and backward-propagation; generating (690, 910) a plurality of output test vectors from the plurality of forward-reached-transition environments and the plurality of backward-reached-transition environments; outputting the plurality of output test vectors; and verifying the software using the output test vectors.