An abstract trace may be defined based on a coverage goal. An execution of a System Under Test (SUT) is guided in accordance with the coverage goal. Non-deterministic decision, which correlates to receiving a stimulus to the SUT, is decided based on a probability function. After one or more executions, the probability function is modified based on a measurement of similarity between the abstract trace and each of the one or more executions. The modification of the probability function may be performed using on Cross-Entropy method. The modification is performed in order to cause determination of non-deterministic decisions in executions to better correlate with the abstract trace. In some exemplary embodiments, a determination whether the abstract trace is reachable is determined based on a rate of convergence of the executions to the abstract trace.