PV1 AProVEanalyses programs for termination

AProVE is a system for automatic termination and complexity analysis of C, Java, Haskell, Prolog, and several forms of rewrite systems

Application domain/field

Type of tool

Termination & complexity analyzer

Expected input



C, Java, Haskell, Prolog or a rewrite system. Also described in more detail on: https://aprove.informatik.rwth-aachen.de/download

Expected output

YES, NO, MAYBE, TIMEOUT indicating whether it could prove termination for the given system.
C Complexity Haskell Java Prolog Termination


Related papers

Last publication date

August 2017

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.