Empirical Evaluation of: Proving Non-Termination via Loop Acceleration

Running our Tool LoAT

• Invocation: loat-static --timeout $TIMEOUT --nonterm $INPUT
• LoAT can parse three different input formats:
• .koat (recommended)
  the format from the category Complexity of Integer Transition Systems of the anual Termination and Complexity Competition
• .smt2
  the format from the category Termination of Integer Transition Systems of the anual Termination and Complexity Competition
• .t2 (experimental)
  the native format of the tool T2

Evaluation

• Evaluation on Integer Programs
• LoAT
• LoAT-LB
• T2
• VeryMax
• AProVE
• Ctrl
• iRankFinder
• Evaluation on the non-linear integer programs from the Anant-benchmarks
• LoAT
• Evaluation on C programs
• LoAT
• AProVE
• Ultimate
• VeryMax