PV4 Ultimate Automizerchecks user-specified properties and some built-in properties, e.g. memory safety, of a C program for a specified architecture

Ultimate Automizer is a software verifier that implements an automata-based approach for the verification of safety and liveness properties

Application domain/field

Type of tool

Model checker

Expected input


Expected output

Whether the property holds or not. It may generate a violation or correctness witness to witness.graphml.


Ultimate Automizer can analyse the reachability of error functions, memory safety, absence of overflows and termination. Built on top of Ultimate, a program analysis framework. Uses Z3, CVC4, MathSAT


License information: https://github.com/ultimate-pa/ultimate/wiki/License


Related papers

Last publication date

14 April 2018

ProVerB specific

Markdown description: view/edit

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