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

Format:

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.

Internals

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

Comments

License: LGPLv3
C Model checking

Links

Last commit date

10 October 2021 (this is for the complete Ultimate framework, it is unclear when the Taipan part is last updated)

Related papers

Last publication date

17 April 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.