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

Automizer Boogie C

Verification of safety properties based on an automata-theoretic approach to software verification.

Büchi Automizer Boogie C

Termination analysis based on Büchi automata.

GemCutter Boogie C

A verifier for concurrent programs based on commutativity – the observation that for certain statements, the execution order does not matter.

Kojak Boogie C

A software model checker.

Taipan Boogie C

Verification of safety properties using trace abstraction and abstract interpretation on path programs.

An LTL software model checker based on Büchi programs.

Lasso Ranker Boogie C

Synthesis of ranking functions and nontermination arguments.

Automata Library automata_script

Nested Word Automata, Büchi Nested Word Automata, Petri Net, Alternating Finite Automata, Tree Automata.

Referee Boogie C

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.