Reo is a channel-based exogenous coordination language.


Reo has an extensive tool development history. We include a selected overview.

Reo compiler

Our most recent Reo compiler maps a textual specification of some Reo connectors to an implementation in a target language of choice. The current version of the compiler supports code generation for Java, Promela (the input language for the SPIN model checker), and Maude. The compiler can be easily extended to support additional target languages.

The compiler is still in development. You are invited to contribute. For instructions on the installation and usage of the compiler, we refer to the documentation available here.

The Extensible Coordination Tools (ECT)

The Extensible Coordination Tools (ECT) are a set of plug-ins for the ​Eclipse platform. The ECT supports:

The figure below shows a so-called ‘alternator’ connector that was designed using the graphical editor of the ECT, and also shows the subsequently automatically generated animation.


The ECT is officially deprecated, in part because we intend to eliminate the dependencies on Eclipse and Flash. Nonetheless, it is still instructive to read the legacy documentation, as it showcases how Reo has been (and can be) applied.


ReoLive aims at compiling a set of Java/Scala based Reo related tools, using a web frontend to interact with them. ReoLive is lightweight in that only an offline Internet browser with JavaScript support is required to use it. For more complex operations, a client-server architecture is also supported.

The source code for the project is available at the ReoLive GitHub repository, and a functional snapshot can be found here, which already supports a graphical Reo circuit editor and conversions into automata and the mCRL2 model checking language. For more information, also see [1].


Dreams (an acronym for ‘distributed runtime evaluation of atomic multiple steps’), also called the Distributed Reo Engine, is a decentralised, actor-based framework in which coordination primitives execute in a distributed environment. The framework decouples certain executions within Reo circuits, achieving greater scalability and allowing for more flexible reconfigurations.

The framework is no longer maintained. For more information, see [2], [3] or the information on the legacy website. Related source code is available at the GitHub repositories ip-constraints and picc.

The Vereofy model checker

Vereofy is a formal verification tool developed by the TU-Dresden in the context of the EU project ​Credo and the DFG/NWO-project ​SYANCO. The model checker can be used as a stand-alone tool, or via an Eclipse plug-in that integrates with the ECT. For more information on Vereofy, visit the official homepage.


  1. Rúben Cruz and José Proença. 2018. ReoLive: Analysing Connectors in Your Browser. In Software Technologies: Applications and Foundations - STAF 2018 Collocated Workshops, Toulouse, France, June 25-29, 2018, Revised Selected Papers, 336–350. doi:10.1007/978-3-030-04771-9_25

  2. José Proença, Dave Clarke, Erik De Vink, and Farhad Arbab. 2012. Dreams: a framework for distributed synchronous coordination. In Proceedings of SAC 2012, 1510–1515. doi:10.1145/2245276.2232017

  3. José Proença. 2011. Synchronous Coordination of Distributed Components (PhD thesis). Universiteit Leiden. hdl:1887/17624