PV1 ⊧ HipTNT+analyses imperative programs for termination

HipTNT+ is a modular termination and non-termination analyzer for imperative programs

Application domain/field

• Termination analysis
• Non-termination
• Imperative programs

Type of tool

Termination prover?

Expected input

• C program
• Optional: Specification

Expected output

TRUE, FALSE and a witness, or UNKNOWN. The witness (+FALSE) represents a counterexample to termination. TRUE indicates that the program will terminate.

Internals

HipTNT+ is built upon the HIP/SLEEK toolset. Uses Omega Calculator and Z3.