ULTIMATE
Automizer
description

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 (website available soon)
Web Interface

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

Open interface
Awards
  • Ultimate Automizer won the overall ranking at the SV-COMP 2017
  • Ultimate Automizer won the overall ranking at the SV-COMP 2016
  • Ultimate Automizer was second in the overall ranking at the SV-COMP 2015
Download

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

SV-COMP

  • Ultimate Automizer for SV-COMP 2017
  • Ultimate Automizer for SV-COMP 2016.

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

Eclipse CDT

We are planing to release an Eclipse CDT plugin that is able to use all toolchains of Ultimate.

Example

A commented automata script file that explains some aspects of our verification approach for recursive programs is available in the web interface of our automata library.

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