PV3 VeryMaxchecks (non-)termination of integer transition systems or C programs, or checks assertions in a C program

Program analysis toolkit for (non-)termination analysis and safety checker

Application domain/field

Expected input

Program or integer transition system


Program: Small fragment of C or C++ with assertion(s) Integer transition system: T2 or Pushdown SMT-LIB2 specification format


VeryMax uses conditional termination arguments to segment the state space for the remainder of the analysis. VeryMax can be used as a safety analyzer and a (non-)termination prover. Uses Barcelogic.


There are two versions available of VeryMax via the project page. The most recent version is the version that provides (non-)termination analysis. The older version provides a safety checker.


Project page: https://www.cs.upc.edu/~albert/VeryMax.html

Related papers

Last publication date

31 March 2017

Related tools

Other tools that participated in the termination category of SV-COMP 2016: AProVE, Ctrl, HipTNT+, SeaHorn, Ultimate

ProVerB specific

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