VeryMax Program Analysis Toolkit

Developed by Critina Borralleras, Daniel Larraz, José Miguel Rivero, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio

Available Tool versions

• Termination prover

  This version of VeryMax provides termination and non termination analysis and it is available as a binary compiled for Linux x64.

  News: VeryMax won the C Integer Programs and Integer Transition Systems categories of the 2016 International Termination and Complexity Competition.

  Some experiments run in StarExec are available:
  • Results of VeryMax on the Integer Transition Systems category. It provides a performance comparison of different configurations for non-termination analysis combined with conditional termination.
  • Results of VeryMax on the C Integer Programs category.
  • Results of VeryMax on a subset of the benchmarks of the SV-COMP Termination category.

• Safety analyzer ("Compositional Safety Verification with Max-SMT" FMCAD2015)

  This version of VeryMax provides a safety checker and it is available as a binary compiled for Linux x64.

  The C++ version of all benchmarks is also included with the binaries. Check the README file for some help about the usage of the tool.

This reasearch is partially supported by

• Spanish MINECO under the grant TIN2013-45732-C4-3-P (project DAMAS) and the FPI grant BES-2011-044621 (Daniel Larraz)
• Spanish MINECO/FEDER under the grant TIN2015-69175-C4-3-R (project LoBaSS)