HipTNT+: A termination and non-termination analyzer by second-order abduction

Abstract

HipTNT+ is a modular termination and non-termination analyzer for imperative programs. For each given method, the analyzer first annotates it with an initial specification with second-order unknown predicates and then incrementally derives richer known specifications with case analysis. Subsequently, the final inference result indicates either (conditional) termination, non-termination, or unknown. During the proving process, new conditions for the case analysis are abductively inferred from the failure of both termination and non-termination proof, which aim to separate the terminating and non-terminating behaviors for each method. This paper introduces the verification approach and the structure of HipTNT+, and instructs how to set up and use the system.