Model checking for Synchronous Java

In this paper, we present a model-checking toolset for a synchronous version of the Java language (Synchronous Java or in short sJava). The toolset includes a set of extensions to the Bandera and Bogor model-checking frameworks. It inherits thus a large number of advantages and features implemented in Bandera and Bogor. It supports the verification of the source models that are directly written in sJava. We developed a new algorithm for optimizing the synchronization tasks between threads. The toolset also generates the outputs that help developers to understand the source of errors and to correct the implementation of the input models in case of failure