Kojak

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

Web interface

Ultimate Kojak is available via a web interface.

Developers

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

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 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.