K. Azadbakht, F.S. de Boer & E.P. de Vink
Deadlock Detection for Actor-Based Coroutines

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.