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)
Ultimate Automizer is available via a web interface in which you can verify C programs.
- 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
We try to provide regular releases for Windows and Linux at our GitHub release page.
SV-COMP
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.
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.
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.
[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