The actor-based language studied in this paper features asynchronous method calls and supports coroutines which allow for the cooperative scheduling of the method invocations belonging to an actor. We model the local behavior of an actor as a well-structured transition system by means of predicate abstraction and derive the decidability of the occurrence of deadlocks caused by the coroutine mode of method execution.

, , , ,
Lecture Notes in Computer Science
International Symposium on Formal Methods
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Azadbakht, K., de Boer, F., & de Vink, E. (2018). Deadlock detection for actor-based coroutines. In Proceedings of the International symposium on Formal Methods (pp. 39–54). doi:10.1007/978-3-319-95582-7_3