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




Menu




(Online) Examples






News

  • [08/06/15] HipTNT+ won the C Integer Programs category (summary result) in the annual Termination Competition 2015, affiliated with the CADE-25 conference.
  • [06/04/15] The research paper about HipTNT+, "Termination and Non-termination Specification Inference", has been published online (doi>10.1145/2737924.2737993).
  • [05/30/15] 1-min video abstract of HipTNT+ is added.
  • [04/04/15] HipTNT+ passed the PLDI 2015 Artifact Evaluation.
  • [03/24/15] Some online heap examples adapted from the TPDB Java Bytecode benchmarks have been added. Please try them.
  • [02/02/15] The research paper of HipTNT+ has been accepted at PLDI 2015.
  • [12/23/14] HipTNT+ won the Bronze medal in the Termination category
    The 4th Intl. Competition on Software Verification (SV-COMP'15) held at TACAS 2015.

Overview

HipTNT+ is an inference system for automatically reasoning about termination and non-termination properties of programs on a per method basis. The system has been built on top of HipTNT, a verification system for program termination and non-termination, to include the capability of automated inference of a case-based termination and non-termination specification for each method. The inferred specification captures multiple scenarios (or pre-conditions) for either
  • termination (denoted by Term with a lexicographic ranking function) or
  • non-termination (denoted by Loop) or
  • unknown (denoted by MayLoop) if the inference mechanism is unable to make a definite decision.
Research papers that describe the system are:
  • Termination and Non-Termination Specification Inference
    Ton Chanh Le, Shengchao Qin and Wei-Ngan Chin
    The 36th annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), ACM, Portland, Oregon, United States, June 13 - 17, 2015.
    [Show/Hide Abstract] [PDF | DOI | BIB | VID]

  • A Resource-Based Logic for Termination and Non-Termination Proofs
    Ton Chanh Le, Cristian Gherghina, Aquinas Hobor and Wei-Ngan Chin
    The 16th International Conference on Formal Engineering Methods (ICFEM'14), Springer-Verlag, Luxembourg, Nov 3 - 7, 2014.
    [Show/Hide Abstract] [WWW | PDF | DOI | BIB]

Downloads and Instructions

Latest HipTNT+'s virtual machine (all-in-one ~1.2GB) - with HipTNT+ and prerequisite software pre-installed.

Latest HipTNT+'s bundle (64-bit executables, examples, and benchmarks ~24MB)

Example programs (on the left panel) and examples from the SV-COMP'15 termination-* benchmarks can be run ONLINE. More example programs and benchmarks can be downloaded from our Download page.

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




Last Update: 06/06/15 by Ton Chanh Le.