Ultimate
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.
Ultimate 套件的环境很难配，至少在国内的网络环境下不太容易，可参考以下心得：