If the program only consists of a single class, one can enter the Java program directly in a window of the web interface. The system then tries to prove (non-)termination of the main method of that class.
To analyze more complex programs (of several classes), the web interface takes an arbitrary jar-file as input. As in the
International Termination Competition, it then tries to prove (non-)termination of the main method of the class that is indicated in the file META-INF/MANIFEST.MF. For details, please see the definition of JBC termination problems. In order to prove (non-)termination of a specific method, one therefore has to add an appropriate main method calling the specific method with random inputs.
The tables below summarize our experiments. They show that for all example sets, AProVE currently yields the most precise results both for termination and non-termination analysis. (However, there are also several examples where Julia and COSTA prove termination whereas AProVE fails.)
In the following table, we give the results of our experiments for the the different sets of examples. Y gives the number of examples where termination was proven, N gives the number of examples where non-termination was proven, M means that the proof failed in less than 60 seconds, T gives the number of examples where the tool took longer than 60 seconds, and R gives the average runtime. By clicking on the name of the example set, you can inspect the details of the respective experiments.
| Example Set | Size | AProVE | AProVE 2011 | Julia | COSTA | ||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Y | N | M | T | R | Y | N | M | T | R | Y | N | M | T | R | Y | N | M | T | R | ||
| Full Set | 387 | 267 | 81 | 11 | 28 | 9.5 | 225 | 81 | 45 | 36 | 11.4 | 191 | 22 | 174 | 0 | 4.7 | 160 | 0 | 181 | 46 | 11.0 |
| TPDB | 268 | 213 | 28 | 5 | 22 | 9.4 | 204 | 28 | 12 | 24 | 11.3 | 163 | 22 | 83 | 0 | 4.4 | 134 | 0 | 117 | 17 | 7.9 |
| Paper + List Reversal | 7 | 7 | 0 | 0 | 0 | 4.4 | 2 | 0 | 4 | 1 | 13.8 | 0 | 0 | 7 | 0 | 3.5 | 1 | 0 | 6 | 0 | 3.7 |
| LinkedList + HashMap | 60 | 51 | 0 | 6 | 3 | 15.8 | 23 | 0 | 29 | 8 | 18.3 | 32 | 0 | 28 | 0 | 8.2 | 29 | 0 | 5 | 26 | 30.4 |
| Nonterm. Evaluation | 57 | 1 | 53 | 0 | 3 | 4.9 | 1 | 53 | 0 | 3 | 4.9 | 1 | 0 | 56 | 0 | 3.1 | 1 | 0 | 53 | 3 | 5.3 |
| Method signature | Example name |
|---|---|
| clear() | juHashMapCreateClear.jar |
| clone() | - (uses native method java.lang.Object.clone()) |
| containsKey(Object key) | juHashMapCreateContainsKey.jar |
| containsValue(Object value) | juHashMapCreateContainsValue.jar |
| equals(Object o) | juHashMapCreateEquals.jar |
| entrySet() | juHashMapCreateIteratorEntryLoop.jar (also iterates once over entry set) |
| get(Object key) | juHashMapCreateGet.jar |
| hashCode | - (uses native method java.lang.Object.hashCode()) |
| isEmpty() | juHashMapCreateIsEmpty.jar |
| keySet() | juHashMapCreateIteratorKeyLoop.jar (also iterates once over key set) |
| put(K key, V value) | juHashMapCreatePut.jar |
| putAll(Map<? extends K, ? extends V> m) | juHashMapCreatePutAll.jar |
| remove(Object key) | juHashMapCreateRemove.jar |
| size() | juHashMapCreateSize.jar |
| values() | juHashMapCreateIteratorValueLoop.jar (also iterates once over value set) |
| toString | - (uses String concatenation) |
| Method signature | Example name |
|---|---|
| add(E e) | juLinkedListCreateAdd.jar |
| add(int index, E element) | juLinkedListCreateAddAt.jar |
| addAll(Collection<? extends E> c) | juLinkedListCreateAddAll.jar |
| addAll(int index, Collection<? extends E> c) | juLinkedListCreateAddAllAt.jar |
| addFirst(E e) | juLinkedListCreateAddFirst.jar |
| addLast(E e) | juLinkedListCreateAddLast.jar |
| clear() | juLinkedListCreateClear.jar |
| clone() | - (uses native method java.lang.Object.clone()) |
| contains(Object o) | juLinkedListCreateContains.jar |
| containsAll(Collection<?> c) | juLinkedListCreateContainsAll.jar |
| descendingIterator() | juLinkedListCreateDescendingIteratorLoop.jar (also iterates once over list) |
| element() | juLinkedListCreateElement.jar |
| equals(Object o) | juLinkedListCreateEquals.jar |
| get(int index) | juLinkedListCreateGet.jar |
| getFirst() | juLinkedListCreateGetFirst.jar |
| getLast() | juLinkedListCreateGetLast.jar |
| hashCode() | - (uses native method java.lang.Object.hashCode()) |
| indexOf(Object o) | juLinkedListCreateIndexOf.jar |
| isEmpty() | juLinkedListCreateIsEmpty.jar |
| iterator() | juLinkedListCreateIteratorLoop.jar (also iterates once over list) |
| lastIndexOf(Object o) | juLinkedListCreateLastIndexOf.jar |
| listIterator(int index) | juLinkedListCreateListIteratorLoop.jar (also iterates once over list) |
| offer(E e) | juLinkedListCreateOffer.jar |
| offerFirst(E e) | juLinkedListCreateOfferFirst.jar |
| offerLast(E e) | juLinkedListCreateOfferLast.jar |
| peek() | juLinkedListCreatePeek.jar |
| peekFirst() | juLinkedListCreatePeekFirst.jar |
| peekLast() | juLinkedListCreatePeekLast.jar |
| poll() | juLinkedListCreatePoll.jar |
| pollFirst() | juLinkedListCreatePollFirst.jar |
| pollLast() | juLinkedListCreatePollLast.jar |
| pop() | juLinkedListCreatePop.jar |
| push(E e) | juLinkedListCreatePush.jar |
| remove() | juLinkedListCreateRemove.jar |
| remove(int index) | juLinkedListCreateRemoveAt.jar |
| remove(Object o) | juLinkedListCreateRemoveElement.jar |
| removeAll(Collection<?> c) | juLinkedListCreateRemoveAll.jar |
| removeFirst() | juLinkedListCreateRemoveFirst.jar |
| removeFirstOccurrence(Object o) | juLinkedListCreateRemoveFirstOccurrence.jar |
| removeLast() | juLinkedListCreateRemoveLast.jar |
| removeLastOccurrence(Object o) | juLinkedListCreateRemoveLastOccurrence.jar |
| removeRange(int fromIndex, int toIndex) | juLinkedListCreateRemoveRange.jar |
| retainAll(Collection<?> c) | juLinkedListCreateRetainAll.jar |
| set(int index, E element) | juLinkedListCreateSet.jar |
| size() | juLinkedListCreateSize.jar |
| subList(int fromIndex, int toIndex) | juLinkedListCreateSubList.jar |
| toArray() | juLinkedListCreateToArray.jar |
| toArray(T[] a) | - (uses reflection) |
| toString() | - (uses String concatenation) |
When using the AProVE web interface, please keep in mind that the computer running the web interface is considerably slower (four AMD Opteron CPU cores with 2.2GHz each) than the one used for the experiments. Therefore, a higher timeout of up to 600 seconds is needed to solve all examples that AProVE could solve in the table below. Please also keep in mind that the computer used for the web interface is used by several other applications as well, so the runtimes may vary.