LoAT

Short description of LoAT.

What inputs are supported?

The following input formats are supported:

• Integer Transition Systems
  • the format that is used in the category "Complexity of Integer Transition Systems" at the Termination and Complexity Competition, including some extensions
  • the format that is used in the category "Termination of Integer Transition Systems" at the Termination and Complexity Competition
• C Integer Programs
• Constrained Horn Clauses (CHCs)

What properties can be verified?

• Transition Systems / C Integer Programs
  • non-termination
  • lower bounds on the worst-case runtime complexity
• CHCs
  • (un)satisfiability

What are the tool’s main techniques for the supported (input, property) pairs?

LoAT is based on the ADCL calculus, whose implementation is built upon our calculus for modular loop-acceleration.

What external tools are used? (e.g., compilers, SMT solvers)

• SMT solvers
  • Z3
  • Yices
• the recurrence solver PURRS
• the automata library libFAUDES
• GiNaC for symbolic computations

What is the tool’s URL?

https://loat-developers.github.io/LoAT/

Example(s)

For examples of Transition Systems and C Integer Programs, consider the following categories of the Termination Problem Data Base:

• Complexity_ITS
• Integer_Transition_Systems
• C_Integer

For examples of CHCs, consider the examples from the category LIA-Lin of the CHC competition 2022.

References

The publications on LoAT can be found on LoAT's website.