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.
- SV-COMP 2017
- Ultimate Automizer won the overall ranking.
- Ultimate Büchi Automizer was first in the category Termination.
- Ultimate Automizer was second in the categories MemSafety and Overflows.
- Ultimate Taipan was second in the category SoftwareSystems.
- Ultimate Automizer was third in the categories ReachSafety and SoftwareSystems.
- Ultimate Taipan was third in the category Overflows.
- SV-COMP 2016
- Ultimate Automizer won the overall ranking.
- Ultimate Automizer won the overall falsification ranking.
- Ultimate Büchi Automizer was second in the category Termination.
- Termination Competition 2015
- SV-COMP 2015
- Ultimate Automizer was second in the overall ranking and in the category Recursive.
- Ultimate Büchi Automizer was second in the category Termination.
- Ultimate Kojak was second in the category Arrays.
- Ultimate Automizer was third in the categories Arrays and Sequentialized.
- Termination Competition 2014
- Ultimate Büchi Automizer was second in the category Termination of Programming Languages.
- SV-COMP 2014
- Ultimate Automizer was second in the category Recursive.
- Ultimate Kojak was third in the category Recursive.
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.
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 are
Alexander Nutz
Alex Saukh (web interface, CDT interface, CACSL2Boogie, Büchi minimization)
Arend v. Reinersdorff (predecessor of Ultimate)
Bat-Chen Golden (incremental verification)
Betim Musa (automata script, interpolants from unsatisfiable cores, incremental proof generation, interpolant consolidation, invariant synthesis)
Björn Buchhold (predecessor of Ultimate, the 2.0 version)
Björn Hagemeister (DFA minimization)
Claus Schätzle (procedure inlining, abstract interpretation octagon domain)
Chen Kefei (nested interpolants)
Christian Ortolf (predecessor of Ultimate)
Christian Schilling
Christian Simon (predecessor of Ultimate, the 2.0 version)
Christoph Hofmann (Ultimate in the cloud)
David Zschocke (invariant synthesis)
Daniel Dietsch
Daniel Christiany (NWA)
Daniel Tischner (random automata, DFA minimization, Büchi minimization, NWA minimization)
Daniel Wadehn (delta debugger)
Dennis Wöfling (danger invariants)
Dirk Steinmetz (invariant synthesis)
Dominik Nuber (floating point)
Elisabeth Henkel (MSO solver)
Evren Ermis
Fabian Reiter (Büchi complementation)
Frank Schüssele (abstract interpretation congruence domain, map elimination)
German Fordinal (Webinterface)
Guilherme Schievelbein (floating point)
Jan Leike (NWA, LassoRanker)
Jan Hättig (total interpolation, abstract interpretation polyhedra domain)
Jan Mortensen (NWA, Petri nets)
Jan Oreans (invariant synthesis)
Jeffery Hsu (incremental inclusion)
Jens Stimpfle (NWA minimization)
Jelena Barth (Jung visualization)
Jeremi Dzienian (Temporal Properties)
Julian Jarecki (Petri nets)
Jochen Hoenicke
Jürgen Christ
Justus Bisser (predecessor of Ultimate)
Lars Nitzke (pthreads)
Layla Franke (DFA minimization)
Leonard Fichtner (polynomial terms)
Marc Fuchs (multi-step automata)
Markus Lindenmann (web interface, CDT interface, CACSL2Boogie, Büchi minimization, C memory model)
Markus Pomrehn (formula simplification, alternating automata)
Markus Zeiger (NWA, E-Matching)
Marius Greitschus
Matthias Heizmann
Matthias Keil (Prefuse visualization)
Max Barth (quantifier elimination)
Maximilian Rohland (floating point)
Nico Hauff (MSO solver)
Nicola Sheldrick (predecessor of Ultimate)
Numair Mansur (fault localization)
Robert Jakob (predecessor of Ultimate)
Saskia Rabald (multi-step automata)
Simon Ley (IC3)
Stefan Wissert (Web interface, CDT interface, CACSL2Boogie, IValuations, large block encoding)
Thomas Lang (loop complexity, bitvectors)
Tobias Grugel (tree automata)
Vincent Langenfeld
Xiaolin Wu (Büchi NWA emptiness check, Büchi NWA complementation)
Yu-Wen Chen (alias analysis)
Many plugins in Ultimate require an SMT-LIB compatible theorem prover. We use SMTInterpol.
Ultimate uses Eclipse RCP. Plugins that handle C code depend on Eclipse CDT.