Rebeca (acrónimo de Reactive Objects Language) es un lenguaje de modelado basado en actores con una base formal, diseñado en un esfuerzo por cerrar la brecha entre los enfoques de verificación formal y las aplicaciones reales. Puede considerarse como un modelo de referencia para computación concurrente , basado en una interpretación operacional del modelo de actores. También es una plataforma para desarrollar sistemas concurrentes basados en objetos en la práctica.
Además de tener una forma apropiada y eficiente de modelar sistemas concurrentes y distribuidos, se necesita un enfoque de verificación formal para asegurar su corrección. Rebeca está respaldada por un conjunto de herramientas de verificación. Las herramientas anteriores proporcionaban una interfaz para trabajar con el código de Rebeca y traducir el código de Rebeca a lenguajes de entrada de verificadores de modelos conocidos y maduros (como SPIN y NuSMV) y, por lo tanto, podían verificar sus propiedades. Rebeca, desde 2005, está respaldada por un verificador de modelos directo basado en Modere (el motor de verificación de modelos de Rebeca). Se utilizan técnicas de abstracción y verificación modular para reducir el espacio de estados y hacer posible la verificación de sistemas reactivos complicados. Además de estas técnicas, Modere admite la reducción de orden parcial y la reducción de simetría.