About

Rebeca (Reactive Objects Language) is an actor-based language with a formal foundation, designed in an effort to bridge the gap between formal verification approaches and real applications. It can be considered as a reference model for concurrent computation, based on an operational interpretation of the actor model. It is also a platform for developing object-based concurrent systems in practice.

Besides having an appropriate and efficient way for modeling concurrent and distributed systems, one needs a formal verification approach to ensure their correctness. Rebeca is supported by Rebeca Verifier tool, as a front-end, to translate the codes into existing model-checker languages and thus, be able to verify their properties. Modular verification and abstraction techniques are used to reduce the state space and make it possible to verify complicated reactive systems.

Rebeca is an actor-based language for modeling and verification of reactive systems. Modeling a system in Rebeca requires one to specify reactive-object templates and a finite set of object instances that run in parallel. Properties can be specified in temporal logic. Different approaches are proposed for verifying correctness of these properties.

Members

person

Marjan Sirjani

Professor, School of Computer Science, Mälardalen University, School of IDT, Västerås, Sweden

email marjan.sirjani "at" mdh.se

person

Ramtin Khosravi

Assistant Professor, School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran

email r.khosravi "at" ut.ac.ir

person

Fatemeh Ghassemi

Assistant Professor, School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran

email fghassemi "at" ut.ac.ir

person

Ehsan Khamespanah

Postdoc Researcher, School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran

email r.khosravi "at" ut.ac.ir

person

Ali Jafari

Postdoc Researcher, School of Computer Science, Reykjavik University, Reykjavik, Iceland

email ali11 "at" ru.is

person

Zeynab Sharifi

PhD Student, School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran

email z.sharifi "at" ut.ac.ir

Alumni

person

Amin Shali

email amshali "at" gmail.com

person

Hossein Hojjat

email hh "at" cs.rit.edu

person

Mohammad Mahdi Jaghoori

email Jaghouri "at" cwi.nl

person

Hamideh Sabouri

email h.sabouri "at" ut.ac.ir

person

Mohammad-Javad Izadi

email m.j.izadi "at" ut.ac.ir

person

Zeynab Sabahi Kaviani

email z.sabahi "at" ut.ac.ir

person

Mahsa Varshosaz

email m.varshosaz "at" ut.ac.ir

person

Brynjar Magnusson

email brynjar "at" brynjar.is

person

Haukur Kristinsson

email haukurk "at" ru.is

person

Ala Harirchi

email alaharirchi "at" gmail.com

person

Niloofar Razavi

email razavi "at" cs.toronto.edu

person

Razieh Behjati

email r.behjati "at" ut.ac.ir

person

Hamed Iravanchi

email iravanchi "at" gmail.com

person

Niusha Hakimipour

email new_f_p "at" yahoo.com