Sources of Nondeterminism in AProVE

AProVE Nondeterminism Sources

This is a list of possible sources for nondeterminism in AProVE.

• Concurrency due to the strategy, e.g., the "CombineParallel" or "Any" strategy runs multiple threads in parallel.

• Concurrency issues due to external methods from the Java API or other libraries.

• Using the method .iterator() on java.util.HashSet or the entry set/key set of java.util.HashMap; note that this method is called implicitly by an extended for-loop over a HashSet or a entry set/key set of the HashMap or over

  • Hint for debugging: set a breakpoint on java.util.HashMap#iterator

• Random numbers

• Time

• Implementing the method equals() but no compatible hashCode() method.

  • Hint: You can check for missing hashCode() methods by enabling the corresponding Eclipse warning.