AProVE Web Interface

This is the AProVE Web Interface for the current version of AProVE.

Analysis of Java Bytecode

Please enter a Java problem (i.e., a program conforming to the Termination Competition rules), where the analysis always starts with the main method and user input is only allowed through the String array which is passed as the only parameter of main.
If the program only consists of a single class, you can enter the Java program directly in the window below. The system then tries to analyze the main method of that class.
For more complex programs (of several classes), you have to construct a jar-file conforming to the Termination Competition rules and upload it.

/**
 * This class represents a list. The function get(n) can be used to access
 * the n-th element.
 * @author Marc Brockschmidt
 */
public class CyclicList {
    /**
     * A reference to the next list element.
     */
    private CyclicList next;

public static void main(String[] args) {
        CyclicList list = CyclicList.create(args.length);
        list.get(args[0].length());
    }

/**
     * Create a new list element.
     * @param n a reference to the next element.
     */
    public CyclicList(final CyclicList n) {
        this.next = n;
    }

/**
     * Create a new cyclical list of a length l.
     * @param l some length
     * @return cyclical list of length max(1, l)
     */
    public static CyclicList create(int x) {
        CyclicList last, current;
        last = current = new CyclicList(null);
        while (--x > 0)
            current = new CyclicList(current);
        return last.next = current;
    }

public CyclicList get(int n) {
        CyclicList cur = this;
        while (--n > 0) {
            cur = cur.next;
        }
        return cur;
    }
}

Choose file

Accepted file formats: jar

Upload a File or Text?

Timeout (1 seconds minimum, 300 seconds maximum):

Output format:

HTML

Plain Text

Version AProVE2023