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. Se puede considerar como un modelo de referencia para el cómputo concurrente, basado en una interpretación operativa del modelo actor. También es una plataforma para desarrollar en la práctica sistemas concurrentes basados en objetos.
Además de tener una forma apropiada y eficiente para modelar sistemas concurrentes y distribuidos, se necesita un enfoque de verificación formal para garantizar su corrección. Rebeca se apoya en un conjunto de herramientas de verificación. Las herramientas anteriores proporcionaron una interfaz para trabajar con el código de Rebeca y para 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, pudieron verificar sus propiedades. Rebeca, desde 2005, se apoya en un verificador de modelos directo basado en Modere (el motor de verificación de modelos de Rebeca). Se utilizan técnicas modulares de verificación y abstracción para reducir el espacio de estado 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.