required - free
counter automata, model checking, reachability analysis, emptiness problem
FLATA is a toolset for the manipulation and the analysis of non-deterministic integer programs (also known as counter automata). FLATA checks emptiness of the model and transforms the input model to a smaller model with equivalent emptiness problem.
Free software under the terms of GNU LGPL (cf. http://www.gnu.org/licenses/lgpl.html).