a tool for analysis (verification of reachability and termination properties) of counter systems (a.k.a. counter automata, integer programs, numerical systems)