Program
Verification
Book

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

Termination
Non-termination

Type of tool

Termination & complexity analyzer

Expected input

Program

Format:

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

Links

Repository (only has releases, not the code): https://github.com/aprove-developers/aprove-releases
Project page: http://aprove.informatik.rwth-aachen.de/
Last commit date: 30 Nov 2022 (default branch)
Last commit date: 30 Nov 2022 (last activity)

Related papers

AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (TACAS '17)
Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution (Journal of Logical and Algebraic Methods in Programming '18)
Complexity Analysis for Java with AProVE (IFM '17)

Last publication date

August 2017

ProVerB specific

Markdown description: view/edit
Reason for this entry: TACAS 2017
Contained in the ProVerB22 dataset (paper + artefact)

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