Getting Started

What MoAT takes as input, what its answers mean, and which components it relies on.

Download and installation instructions are not yet published here.

Once MoAT is distributed, this page will describe how to obtain and run it. In the meantime, see GitHub or the publications page.

Input

An integer transition system

MoAT analyzes programs modeled as ITSs: a finite set of variables, a finite set of locations with a designated initial and terminal location, and a finite set of transitions carrying a guard and an update. In the evaluation, the C benchmarks from SV-COMP and TermComp were translated into ITSs before running MoAT.

An LTL formula

The property to verify. MoAT negates it, builds a Büchi automaton for the negation, and forms the synchronized product with the ITS. The evaluation used four property classes: Reach-Avoid, Overflow, Recurrence, and Progress.

Output

Yes

The property is verified. The product ITS is fairly terminating, proved by KoAT on the incoming transitions of the fair locations.

The property is refuted. LoAT found a reachable non-terminating cycle containing a fair location; the trace is projected back to the locations of the original ITS to give a counterexample.

Unknown

Fair termination is undecidable in general, so neither backend may reach a conclusion within the time limit.

Components

MoAT is a framework built on top of existing tools. Running it means running these components:

Spot builds the Büchi automaton for the negated formula
KoAT proves fair termination of the product ITS
LoAT disproves fair termination and yields the counterexample