Taipan

Ultimate Taipan is a software model checker that is implemented in the Ultimate framework.

Web interface

Ultimate Taipan is available via a web interface.

Developers

• Daniel Dietsch
• Marius Greitschus

Download

We try to provide regular releases for Windows and Linux at our GitHub release page.

All archives available here contain commandline versions of Ultimate Taipan that participate(d) in the Competition on Software Verification (SV-COMP). They are build for x86-64 linux and can be run using the provided Python script Ultimate.py as follows.

Ultimate.py [-h] [--version] [--full-output] [--validate] spec {32bit,64bit} {simple,precise} file [file ...]

Mandatory arguments

• spec
  An property (.prp) file from SVCOMP.
• {32bit,64bit}
  Choose which architecture (defined as per SV-COMP rules) should be assumed.
• {simple,precise}
  Ultimate does not use the distinction between simple and precise memory model and always assumes precise. For compatibility reasons, you have to provide either value.
• file
  Either one C file or one C file and one witness as matching .graphml file.

Optional arguments

• -h, --help
  Show a help message and exit.
• --version
  Print Ultimate Taipan's version and exit.
• --full-output
  Print Ultimate Taipan's full output to stderr after verification ends.
• --validate
  Validate the provided witness