Büchi Automizer

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 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.

Developers

Ultimate Buchi Automizer is maintained by Matthias Heizmann. The built-in tool LassoRanker is maintained by Jan Leike and Matthias Heizmann. Since Ultimate Büchi 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.