Unbeast
Subproject |
S1 |
Categories |
Synthesis tools |
Overview |
Unbeast synthesises finite-state systems from specifications written in linear-time temporal logic (LTL). It combines bounded synthesis, specification splitting and symbolic game solving with binary decision diagrams (BDDs), which allows tackling specifications that previous tools were typically unable to handle. In case of realizability of a given specification, Unbeast computes a prototype implementation in a fully symbolic way, which is especially beneficial for settings with many input and output bits. |
R. Ehlers. Unbeast: Symbolic Bounded Synthesis. In 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 6605 of Lecture Notes in Computer Science (LNCS), pages 272-275, 2011. R. Ehlers. Symbolic bounded synthesis. In T. Touili, B. Cook, and P. Jackson, editors, 22nd International Conference on Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science (LNCS), pages 365-379, 2010. |
|
Benchmarks |
|
Download |
|
Manual |
|
Status |
Prototype |