HipTNT+
HipTNT+: A Termination and Non-Termination Specification Inference System

Ton Chanh Le, Shengchao Qin and Wei-Ngan Chin



Menu




(Online) Examples




Legend

  The method terminates for all inputs (TRUE)

  There is an execution trace or a precondition that leads to definite non-termination (FALSE)

  Otherwise (UNKNOWN)



Contact

Please contact Ton Chanh Le if you have any problems/suggestions/discussions or simply want to learn more about HipTNT+.





Input 


Infer lexicographic ranking function Disable post condition inference

Results

Inference Detail