Ultimate Automizer

• is a software model checker that implements an approach based on automata [1,2,3,4]
• is one toolchain of the Ultimate software analysis framework
• is maintained by Matthias Heizmann
• uses the Ultimate Automata Library

Awards

• Ultimate Automizer won the overall ranking at the SV-COMP 2024
• Ultimate Automizer won the overall ranking at the SV-COMP 2023
• Ultimate Automizer won the overall ranking at the SV-COMP 2017
• Ultimate Automizer won the overall ranking at the SV-COMP 2016

Web Interface

Ultimate Automizer is available via a web interface in which you can verify C programs.

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 Automizer 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 Automizer's version and exit.
• --full-output
  Print Ultimate Automizer's full output to stderr after verification ends.
• --validate
  Validate the provided witness

Developers

Since Ultimate Automizer is a toolchain of the Ultimate software analysis framework, many people were involved in the development (especially our bachelor and master students). If you are a student at our university and you like to contribute to Ultimate in a project, laboratory, or thesis then contact Matthias Heizmann or any other Ultimate developer.

Related Publications

[1] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model Checking for People Who Love Automata. CAV 2013:36-52
[2] Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, Andreas Podelski: Ultimate Automizer with SMTInterpol - (Competition Contribution). TACAS 2013:641-643
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Nested interpolants. POPL 2010:471-482
[4] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Refinement of Trace Abstraction. SAS 2009:69-85