HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction
Ton Chanh Le, Quang-Trung Ta, Wei-Ngan Chin
Published in The 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems: SV-COMP (SV-COMP@TACAS), 2017
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.