Ultimate Büchi Automizer implements a novel approach to termination analysis in which a program is decomposed into modules. Each module represents a set of traces that share a common termination argument. The decomposition is constructed on demand by “learning” terminating modules from a termination analysis of lasso-shaped sample traces. For this termination analysis of lasso-shaped traces the built-in tool LassoRanker is used.
Ultimate Automizer is available via a web interface in which you can analyse termination of C programs. This version has some limitations. We use a theorem prover that does not support non-linear arithmetic and therefore the built-in tool LassoRanker can only provide linear ranking functions.
Ultimate Büchi Automizer and the built-in tool LassoRanker are in heavy development. A recent version is available on request, please contact Matthias Heizmann.
Commandline Version (CAV 2014 Submission)
The commandline version that was used for the evaluation in our CAV 2014 submission is available. This version runs on x86-64 linux machines and has some limitations. In our evaluation we showed the potential ouf our method to prove termination of a general program while using only simple termination arguments for lasso-shaped traces. Therefore, we restricted the built-in tool LassoRanker to linear ranking functions.
Commandline Version (SV-COMP 2014)
The commandline version that was our competition candidate for the demonstration category on termination at the SV-COMP 2014. This version runs on x86-64 Linux machines and requires that the theorem prover Z3 is installed. In this version, the built-in tool LassoRanker is limited to linear ranking functions and multiphase ranking functions.