- [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.
- 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.
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]
Abstract: Techniques for proving termination and non-termination of imperative programs are usually considered as orthogonal mechanisms. In this paper, we propose a novel mechanism that analyzes and proves both program termination and non-termination at the same time. We first introduce the concept of second-order termination constraints and accumulate a set of relational assumptions on them via a Hoare-style verification. We then solve these assumptions with case analysis to determine the (conditional) termination and non-termination scenarios expressed in some specification logic form. In contrast to current approaches, our technique can construct a summary of terminating and non-terminating behaviors for each method. This enables modularity and reuse for our termination and non-termination proving processes. We have tested our tool on sample programs from a recent termination competition, and compared favorably against state-of-the-art termination analyzers.
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]
Abstract: We propose a unified logical framework for specifying and proving both termination and non-termination of various programs. Our framework is based on a resource logic which captures both upper and lower bounds on resources used by the programs. By an abstraction, we evolve this resource logic for execution length into a temporal logic with three predicates to reason about termination, non-termination or unknown. We introduce a new logical entailment system for temporal constraints and show how Hoare logic can be seamlessly used to prove termination and non-termination in our unified framework. Though this paper's focus is on the formal foundations for a new unified framework, we also report on the usability and practicality of our approach by specifying and verifying both termination and non-termination properties for about 300 programs, collected from a variety of sources. This adds a modest 5-10% verification overhead when compared to underlying partial-correctness verification system.
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)
Last Update: 06/06/15 by Ton Chanh Le.