Afra
Integrated Verification Environment for Rebeca/Timed Rebeca/SystemC
RMC
Command Line Model Checker of Rebeca Family Models
Jacco
State Space Generator of Java Actor Programs (which are written by Actor Foundry)
ReGen
Hadoop YARN and Natjam-R job dispatch and eviction simulator using Timed Rebeca. Computes the efficency of deadline based scheduling in the presence of preemption.
Timed Rebeca to RTMaude
Analysis toolset of Timed Rebeca, using Real-Time Maude as backend model checker
Probabilistic Timed Rebeca Analysis
Analysis toolset for Probabilistic Timed Rebeca models, using RMC for creating the state space and PRISM or IMCA for the performance evaluation of the models.

Statistical Model Checking of Timed Rebeca Models
The toolset and some examples for statistical model checking of Timed Rebeca models, using McErlang
Rebeca to Erlang
Rebeca to Erlang
Sarir
Rebeca to mCRL2 translator
Rebeca Distributed Model Checker
Distributed Model Checker for Rebeca
Rebeca Verifier
Integrating R2SMV, R2P, and component-based model checking
ReUML
UML model Verifier using Rebeca toolset
Rebeca to Promela
A Translator for Rebeca Models to Promela
Rebeca to SMV
A Translator for Rebeca Models to SMV