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.

Web Interface

Ultimate Automizer is available via a 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.

screenshot of web interface

Commandline Version

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.

Developers

Ultimate Buchi Automizer is maintained by Matthias Heizmann. The built-in tool LassoRanker is maintained by Jan Leike and Matthias Heizmann. Since Ultimate Buchi Automizer is a toolchain of the Ultimate software analysis framework, many people contributed code and ideas. We want to mention especially, Jürgen Christ, Daniel Dietsch, Jochen Hoenicke, Markus Lindenmann, Betim Musa, Alexander Nutz, Christian Schilling, Stefan Wissert, and Andreas Podelski.