LoAT (Loop Acceleration Tool) is a fully automated tool to analyze transition systems and linear Constrained Horn Clauses (CHCs) with integer variables. For transition systems, it supports the inference of lower bounds on the worst-case runtime complexity and non-termination proving. For CHCs, it can prove unsatisfiability.
For more information, please visit LoAT's website.