PV4 Ultimate Taipanchecks properties of a C program for a specified architecture and memory model

Ultimate Taipan is a software model checker which combines trace abstraction and abstract interpretation

Application domain/field

Type of tool

Software model checker

Expected input


Expected output

Whether the specification holds. If it does not hold then it will store a human readable counterexample in the file UltimateCounterExample.errorpath and a violation witness to witness.graphml. If passed the argument --validate then it will validate the provided witness.


Implemented on top of the program analysis framework Ultimate. Uses Z3 and CVC4


License: LGPLv3
C Model checking


Related papers

Last publication date

17 April 2020

ProVerB specific

Markdown description: view/edit

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