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

• Termination
• Safety verification

Expected input

Program or integer transition system

Format:

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

Internals

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.

Comments

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.