Towards the automated verification of multithreaded Java programs

In this paper we investigate the possible application of parameterized verification techniques to synchronization skeletons of multithreaded Java programs. As conceptual contribution, we identify a class of infinite-state abstract models, called Multi-Transfer Nets (MTNs), that preserve the main features of the semantics of concurrent Java. We achieve this goal by exploiting an interesting connection with the Broadcast Protocols of [7], and by introducing the notion of asynchronous rendez-vous. As technical contribution, we extend the symbolic verification techniques of [6] based on Covering Sharing Trees and structural invariants to MTNs. As practical contribution, we report on experimental results for verification of examples of multithreaded Java programs. © Springer-Verlag Berlin Heidelberg 2002.SCOPUS: cp.k