Symmetry and partial order reduction techniques in model checking Rebeca. - Mohammad Mahdi Jaghoori; Marjan Sirjani; Mohammad Reza Mousavi 001; Ehsan Khamespanah; Ali Movaghar 001 (Acta Informatica, 2010)

Sysfier: Actor-based formal verification of SystemC. - Niloofar Razavi; Razieh Behjati; Hamideh Sabouri; Ehsan Khamespanah; Amin Shali; Marjan Sirjani (ACM Trans. Embed. Comput. Syst., 2010)

Timed-rebeca schedulability and deadlock-freedom analysis using floating-time transition system. - Ehsan Khamespanah; Zeynab Sabahi-Kaviani; Ramtin Khosravi; Marjan Sirjani; Mohammad-Javad Izadi (AGERE!@SPLASH, 2012)

Analysing timed Rebeca using McErlang. - Haukur Kristinsson; Ali Jafari; Ehsan Khamespanah; Brynjar Magnusson; Marjan Sirjani (AGERE!@SPLASH, 2013)

Formal Semantics and Analysis of Timed Rebeca in Real-Time Maude. - Zeynab Sabahi-Kaviani; Ramtin Khosravi; Marjan Sirjani; Peter Csaba Ölveczky; Ehsan Khamespanah (FTSCS, 2013)

Efficient TCTL Model Checking Algorithm for Timed Actors. - Ehsan Khamespanah; Ramtin Khosravi; Marjan Sirjani (AGERE!@SPLASH, 2014)

Event-Based Analysis of Timed Rebeca Models using SQL. - Brynjar Magnusson; Ehsan Khamespanah; Ramtin Khosravi; Marjan Sirjani (AGERE!@SPLASH, 2014)

Performance Analysis of Distributed and Asynchronous Systems using Probabilistic Timed Actors. - Ali Jafari; Ehsan Khamespanah; Marjan Sirjani; Holger Hermanns (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014)

Jacco: more efficient model checking toolset for Java actor programs. - Arvin Zakeriyan; Ehsan Khamespanah; Marjan Sirjani; Ramtin Khosravi (AGERE!@SPLASH, 2015)

Floating Time Transition System: More Efficient Analysis of Timed Actors. - Ehsan Khamespanah; Marjan Sirjani; Mahesh Viswanathan 001; Ramtin Khosravi (FACS, 2015)

State Distribution Policy for Distributed Model Checking of Actor Models. - Ehsan Khamespanah; Marjan Sirjani; Mohammad Reza Mousavi 001; Zeynab Sabahi-Kaviani; Mohamadreza Razzazi (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015)

Timed Rebeca schedulability and deadlock freedom analysis using bounded floating time transition system. - Ehsan Khamespanah; Marjan Sirjani; Zeynab Sabahi-Kaviani; Ramtin Khosravi; Mohammad-Javad Izadi (Sci. Comput. Program., 2015)

Formal semantics and efficient analysis of Timed Rebeca in Real-Time Maude. - Zeynab Sabahi-Kaviani; Ramtin Khosravi; Peter Csaba Ölveczky; Ehsan Khamespanah; Marjan Sirjani (Sci. Comput. Program., 2015)

On Time Actors. - Marjan Sirjani; Ehsan Khamespanah (Theory and Practice of Formal Methods, 2016)

Coordinated Actors for Reliable Self-adaptive Systems. - Maryam Bagheri 001; Ilge Akkaya; Ehsan Khamespanah; Narges Khakpour; Marjan Sirjani; Ali Movaghar 001; Edward A. Lee (FACS, 2016)

Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking. - Ehsan Khamespanah; Kirill Mechitov; Marjan Sirjani; Gul A. Agha (SPIN, 2016)

Statistical model checking of Timed Rebeca models. - Ali Jafari; Ehsan Khamespanah; Haukur Kristinsson; Marjan Sirjani; Brynjar Magnusson (Comput. Lang. Syst. Struct., 2016)

PTRebeca: Modeling and analysis of distributed and asynchronous systems. - Ali Jafari; Ehsan Khamespanah; Marjan Sirjani; Holger Hermanns; Matteo Cimini (Sci. Comput. Program., 2016)

LeeTL: LTL with quantifications over model objects. - Pouria Mellati; Ehsan Khamespanah; Ramtin Khosravi (SPIN, 2017)

A Survey of Active Object Languages. - Frank S. de Boer; Vlad Serbanescu 001; Reiner Hähnle; Ludovic Henrio; Justine Rochas; Crystal Chang Din; Einar Broch Johnsen; Marjan Sirjani; Ehsan Khamespanah; Kiko Fernandez-Reyes; Albert Mingkun Yang (ACM Comput. Surv., 2017)

Runtime compositional analysis of track-based traffic control systems. - Maryam Bagheri 001; Ehsan Khamespanah; Marjan Sirjani; Ali Movaghar 001; Edward A. Lee (SIGBED Rev., 2017)

A compositional approach for modeling and timing analysis of wireless sensor and actuator networks. - Marjan Sirjani; Ehsan Khamespanah; Kirill Mechitov; Gul Agha (SIGBED Rev., 2017)

Improving the Performance of Actor-Based Programs Using a New Actor to Thread Association Technique. - Fahimeh Rahemi; Ehsan Khamespanah; Ramtin Khosravi (DAIS, 2018)

Coordinated actor model of self-adaptive track-based traffic control systems. - Maryam Bagheri 001; Marjan Sirjani; Ehsan Khamespanah; Narges Khakpour; Ilge Akkaya; Ali Movaghar 001; Edward A. Lee (J. Syst. Softw., 2018)

An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models. - Ehsan Khamespanah; Ramtin Khosravi; Marjan Sirjani (Sci. Comput. Program., 2018)

Modeling and analyzing real-time wireless sensor and actuator networks using actors and model checking. - Ehsan Khamespanah; Marjan Sirjani; Kirill Mechitov; Gul Agha (Int. J. Softw. Tools Technol. Transf., 2018)

An Actor-Based Design Platform for System of Systems. - Marjan Sirjani; Giorgio Forcina; Ali Jafari; Stephan Baumgart; Ehsan Khamespanah; Ali Sedaghatbaf (COMPSAC (1), 2019)

Reactive Actors: Isolation for Efficient Analysis of Distributed Systems. - Marjan Sirjani; Ehsan Khamespanah; Fatemeh Ghassemi (DS-RT, 2019)

Using Reo Formalism for Compliance Checking of Architecture Evolution with Evolutionary Rules. - Zainab Liaghat; MohammadReza Besharati; Mohammad Izadi; Ehsan Khamespanah (SoMeT, 2019)

VeriVANca: An Actor-Based Framework for Formal Verification of Warning Message Dissemination Schemes in VANETs. - Farnaz Yousefi; Ehsan Khamespanah; Mohammed Gharib; Marjan Sirjani; Ali Movaghar 001 (SPIN, 2019)

A Compositional Approach for Reliable Adaptation of Track-based Traffic Control Systems at Runtime. - Maryam Bagheri 001; Marjan Sirjani; Ehsan Khamespanah; Ali Movaghar 001 (CoRR, 2019)

Decentralized Runtime Verification for LTL Properties Using Global Clock. - M. Ali Dorosty; Fathiyeh Faghih; Ehsan Khamespanah (CoRR, 2019)

Developing Safe Smart Contracts. - Sajjad Rezaei; Ehsan Khamespanah; Marjan Sirjani; Ali Sedaghatbaf; Siamak Mohammadi (COMPSAC, 2020)

Model Checking Software in Cyberphysical Systems. - Marjan Sirjani; Edward A. Lee; Ehsan Khamespanah (COMPSAC, 2020)

Towards Formal Analysis of Vehicle Platoons Using Actor Model. - Zeinab Sharifi; Ramtin Khosravi; Marjan Sirjani; Ehsan Khamespanah (ETFA, 2020)

Lightweight Formal Method for Robust Routing in Track-based Traffic Control Systems. - Maryam Bagheri 001; Edward A. Lee; Eunsuk Kang; Marjan Sirjani; Ehsan Khamespanah; Ali Movaghar 001 (MEMOCODE, 2020)

Finite Interval-Time Transition System for Real-Time Actors. - Shaghayegh Tavassoli; Ramtin Khosravi; Ehsan Khamespanah (TTCS, 2020)

Safe Design of Flow Management Systems Using Rebeca. - Giorgio Forcina; Ali Sedaghatbaf; Stephan Baumgart; Ali Jafari; Ehsan Khamespanah; Pavle Mrvaljevic; Marjan Sirjani (J. Inf. Process., 2020)

VeriVANca framework: verification of VANETs by property-based message passing of actors in Rebeca with inheritance. - Farnaz Yousefi; Ehsan Khamespanah; Mohammed Gharib; Marjan Sirjani; Ali Movaghar 001 (Int. J. Softw. Tools Technol. Transf., 2020)

Using Afra in Different Domains by Tool Orchestration. - Ehsan Khamespanah; Pavle Mrvaljevic; Anas Fattouh; Marjan Sirjani (Composing Model-Based Analysis Tools, 2021)

Towards Automatic Test Case Generation for Industrial Software Systems Based on Functional Specifications. - Arvin Zakeriyan; Ramtin Khosravi; Hadi Safari; Ehsan Khamespanah (FSEN, 2021)

Partial Order Reduction for Timed Actors. - Maryam Bagheri 001; Marjan Sirjani; Ehsan Khamespanah; Hossein Hojjat; Ali Movaghar 001 (VSTTE, 2021)

Schedulability Analysis of WSAN Applications: Outperformance of a Model Checking Approach. - Ehsan Khamespanah; Morteza Mohaqeqi; Mohammad Ashjaei; Marjan Sirjani (ETFA, 2022)

Specification and Verification of Timing Properties in Interoperable Medical Systems. - Mahsa Zarneshan; Fatemeh Ghassemi; Ehsan Khamespanah; Marjan Sirjani; John Hatcliff (Log. Methods Comput. Sci., 2022)

Magnifier: A Compositional Analysis Approach for Autonomous Traffic Control. - Maryam Bagheri 001; Marjan Sirjani; Ehsan Khamespanah; Christel Baier; Ali Movaghar 001 (IEEE Trans. Software Eng., 2022)

Model Checking of Hyperledger Fabric Smart Contracts. - Elmira Ebrahimi; Ehsan Khamespanah; Marjan Sirjani; Siamak Mohammadi (ETFA, 2023)

Afra: An Eclipse-Based Tool with Extensible Architecture for Modeling and Model Checking of Rebeca Family Models. - Ehsan Khamespanah; Marjan Sirjani; Ramtin Khosravi (FSEN, 2023)

Transparent Actor Model. - Fatemeh Ghassemi; Marjan Sirjani; Ehsan Khamespanah; Mahrokh Mirani; Hossein Hojjat (FormaliSE, 2023)

Timed Actors and Their Formal Verification. - Marjan Sirjani; Ehsan Khamespanah (EXPRESS/SOS, 2023)

Automated testing of an industrial stock market trading platform based on functional specification. - Arvin Zakeriyan; Ramtin Khosravi; Hadi Safari; Ehsan Khamespanah; Seyede Mehrnaz Shamsabadi (Sci. Comput. Program., 2023)

Actors Upgraded for Variability, Adaptability, and Determinism. - Ramtin Khosravi; Ehsan Khamespanah; Fatemeh Ghassemi; Marjan Sirjani (Active Object Languages: Current Research Trends, 2024)

20 Years of Actor Model Checking with Rebeca From Dining Philosophers to Micro-services. - Ehsan Khamespanah; Mohammad Mahdi Jaghoori (Rebeca for Actor Analysis in Action, 2025)