Ultimate is a program analysis framework. Ultimate consists of several plugins that perform steps of a program analysis, e.g., parsing source code, transforming programs from one representation to another, or analyzing programs. Toolchains of these plugins can perform complex tasks, e.g., verify that a C program fulfills a given specification.
The official website includes a web interface which allows you to use several toolchains online, a list of all developers, and a list of awards Ultimate received over the years.
The available documentation can be found in our wiki.