OOX comes in two parts: the language and a verification tool for this language. The following sections will describe each part separately.

OOX is an intermediate verification language (IVL) with objects and concurrency as first class citizens. The syntax of OOX will be familiar to those experienced with object-oriented languages as e.g. Java and C#.

For example, see the OOX program below. In this program, we have a counter that incremented the field current in the class Counter from its initial value 0 to 4 in a concurrent fashion.

class Counter {
    int current;

    Counter(int initial) {
        this.current := initial; 
    }
        
    void increment() {
        lock(this) {
            int value := this.count;
            this.current := value + 1;
        }
    }

    static void count(int initial, int N)
            requires(initial >= 0)
            exceptional(false) {
        Counter counter := new Counter(initial);
        int i := 0;
        while(i < N) {
            fork counter.increment();
            i := i + 1;
        }
        join;
        int value := counter.current;
        assertvalue == initial + N;
    }
                
    static void main(int initial) { 
        count(initial, 4); 
    }
}

For those interested, OOX also has a formal semantics.

The OOX language comes with a tool to verify such programs with a tool also named OOX. It is based on symbolic execution and supports all language features as defined in the OOX language.

OOX is developed with GHC, and is tested using GHC 8.8.4. It also requires the SMT solver Z3, specifically version 4.8.8.

Simply use the command cabal v2-build to build or cabal v2-repl to interactively use OOX. Cabal will ensure that the required Haskell packages are installed. The Z3 package will require a bit more work, as it requires the Z3 bindings. On Windows, the fields extra-include-dirs and extra-lib-dirs can be added to the Cabal configuration file located in the user-specific AppData.

The OOX verification tool can be tweaked using the following set of parameters.

For example, the command oox "program.oox" -f "Program.main" -k 150 -i 0 verifies the function main in the class Program in the program program.oox up to a maximum depth of 150 with logging disabled.