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

• Daniel Dietsch
• Evren Ermis
• Alexander Nutz
• Mostafa Mahmoud Mohamed

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

SV-COMP

• Ultimate Kojak for SV-COMP 2017
• Ultimate Kojak for SV-COMP 2016
• Ultimate Kojak for SV-COMP 2015
• Ultimate Kojak for SV-COMP 2014

All archives available here contain commandline versions of Ultimate Kojak 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] spec {32bit,64bit} {simple,precise} 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
  One C file.

Optional arguments

• -h, --help
  Show a help message and exit.
• --version
  Print Ultimate Kojak's version and exit.
• --full-output
  Print Ultimate Kojak's full output to stderr after verification ends.