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

• Software model checking
• Model checking

Type of tool

Software model checker

Expected input

• Program
• Specification/property
• Architecture
• Memory model
• Optional: witness

Format:

• Program: one C file.
• Specification: .prp file from SV-COMP
• Architecture: the value 32bit or 64bit
• Memory model: the value precise or simple (this needs to be specified, but the tool always assumes precise)
• Optional witness: .graphml file

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