Unbeast – Symbolic Bounded Synthesis

Copyright © 2010 Rüdiger Ehlers, Saarland University


Synthesis of finite state systems has been proven to be a valuable concept for the development of open systems that are correct by construction Unbeast is a tool for this task capable of handling full linear-time temporal logic (LTL). It is designed for specifications comprising a set of assumptions (which the system under construction can assume to be correct) and a set of guarantees (which the system needs to fulfill). From a technical point of view, Unbeast builds upon the bounded synthesis approach.

Requirements & Instructions

For correct operation of the Unbeast tool, a moderately modern Linux distribution is required. The tool has to be compiled before usage. Under Ubuntu Linux, it should suffice to install the package build-essential.

Additionally, at least one of the following LTL-to-Büchi converters needs to be installed. The converter is called by the Unbeast tool at runtime.

Installation instructions can be found on the respective homepages.

The Unbeast tool uses the CUDD library (v.2.4.1 or greater) for manipulating binary decision diagrams. The file README, which is included in the Unbeast distribution, contains detailed instructions on building Unbeast with CUDD. The usage of the Unbeast tool is also explained in the README file.


[Ehl10c] Rüdiger Ehlers. Symbolic Bounded Synthesis. 22nd International Conference on Computer Aided Verification (CAV 2010).


The prototype is free for use in academic context. For all other purposes, including integration into other tools, please contact the author. Furthermore, the licensing details stated in this document apply.


Note that this tool set is in a prototype stage. Thus, there may be bugs in the implementation. If you find one, please contact the author.


Rüdiger Ehlers