Ultimate is a program analysis framework. Ultimate consists of several plugins that perform steps of an program analysis, e.g., parsing source code, transforming programs from one representation to another, or analyze programs. Toolchains of these plugins can perform complex tasks, e.g., verify that a C program fulfills a given specification.
Tools
Verification of safety properties based on an automata-theoretic approach to software verification.
Termination analysis based on Büchi automata.
A verifier for concurrent programs based on commutativity – the observation that for certain statements, the execution order does not matter.
A software model checker.
Verification of safety properties using trace abstraction and abstract interpretation on path programs.
An LTL software model checker based on Büchi programs.
Synthesis of ranking functions and nontermination arguments.
Nested Word Automata, Büchi Nested Word Automata, Petri Net, Alternating Finite Automata, Tree Automata.
Checking validity of given invariants.
Run SMT script.
Awards
ULTIMATE tools have won many prizes at competitions like the International Competition on Software Verification (SV-COMP) or the Termination Competition. ULTIMATE Automizer has won the Overall ranking of SV-COMP four times (2016, 2017, 2023 and 2024). Find more information here.
Development
The Ultimate source code and some documentation is available at GitHub.
The core of Ultimate and many plugins are subject to the LGPLv3 license with a linking exception to Eclipse RCP and Eclipse CDT.
Developers
The current main developers of Ultimate are:
Daniel Dietsch
Dominik Klumpp
Frank Schüssele
Matthias Heizmann
Most Ultimate developers are students and researchers in the software engineering group of Andreas Podelski at the University of Freiburg.
Current and former developers of Ultimate can be found here.
Development
The Ultimate source code and some documentation is available at GitHub.
The core of Ultimate and many plugins are subject to the LGPLv3 license with a linking exception to Eclipse RCP and Eclipse CDT.