Using Bounded Model Checking with BOGOR

BOGOR model checking framework is developed for Object-Oriented software verification. It represents system as BIR (Bandera Intermediate Language). To model checking BIR, the BOGOR represents state as a node and transition as edge. First, BOGOR generates node and edge. Second, Model checking is performed in graph structure. However, this approach is inefficient to verify large software system. In this paper, we present symbolic model checking techniques to verify efficient BIR model checking. Experimental results show that the proposed algorithm can check more efficiently.