An approach to verify concurrent object-oriented programs

Today, object-oriented methodologies are widely used for developing concurrent distributed systems. There are many well-known object-oriented methodologies and techniques to develop concurrent distributed systems. However, such systems are likely to have bugs. Hence, verification plays an important role in this context. In this paper we propose an approach to verify concurrent object-oriented programs using model checking. To do so, we employ the Bogor model checker. The concurrent programs are translated to BIR- the input language of Bogor- and Bogor performs the verification and shows the existing bugs, if there is any, through counter-examples.