Skip to content
Branch: master
Go to file

Latest commit


Failed to load latest commit information.
Latest commit message
Commit time

Sylvan Build Status

Sylvan is a parallel (multi-core) multi-terminal binary decision diagram library written in C. Sylvan implements parallelized operations on binary decision diagrams supporting any kind of terminal, including standard Booleans, integers, floating points and any user-defined types. Sylvan also implements operations on specialized list decision diagrams for model-checking. Both sequential and parallel BDD-based algorithms can benefit from parallelism. Sylvan uses the work-stealing framework Lace and parallel datastructures to implement scalable multi-core operations on decision diagrams.

Sylvan was initially developed by the Formal Methods and Tools group at the University of Twente as part of the MaDriD project, which was funded by NWO, and further by the Formal Methods and Verification group at the Johannes Kepler University Linz as part of the RiSE project. Sylvan is licensed with the Apache 2.0 license.

The main author of Sylvan is Tom van Dijk who can be reached via Please let us know if you use Sylvan in your projects and if you need decision diagram operations that are currently not implemented in Sylvan.

The main repository of Sylvan is A mirror is available at

Bindings for other languages than C/C++ also exist:

Documentation is available at GitHub Pages.


T. van Dijk (2016) Sylvan: Multi-core Decision Diagrams. PhD Thesis.

T. van Dijk and J.C. van de Pol (2016) Sylvan: Multi-core Framework for Decision Diagrams. In: STTT (Special Issue), Springer.

T. van Dijk and J. van de Pol (2015) Sylvan: Multi-core Decision Diagrams. In: TACAS 2015, LNCS 9035. Springer.

T. van Dijk and A.W. Laarman and J. van de Pol (2012) Multi-Core BDD Operations for Symbolic Reachability. In: PDMC 2012, ENTCS. Elsevier.


Implementation of multi-core (binary) decision diagrams



You can’t perform that action at this time.