PV1 MuValchecks whether a C program will (non-)terminate

Termination analyzer?

Application domain/field

Type of tool

(Non-)termination analyzer

Expected input

C program


.t2 file They provide a command that can be used to convert a .c file into a z.t2 file using llvm2kittel.

Expected output

Indicates whether the tool can prove that the program terminates (YES), the tool verifies non-termination(NO), timed out (TO), or could not find an answer (U).


They focus on synthesizing ranking functions. Ranking functions assign a natural number to each program state, in such a way that the values strictly decrease along transitions. If there is such a ranking function, it can be used to prove the termination of a program. Uses Z3


License: Apache-2.0
C Termination


Related papers

Decision Tree Learning in CEGIS-Based Termination Analysis (CAV '21)

Last publication date

15 July 2021

Related tools

AProVE, iRankFinder, Ultimate Automizer

ProVerB specific

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