Towards Automated Software Verification and Validation

Today, it's an important requirement to have software systems without any bug. Model checking has proven to be a viable solution for reasoning about behavior properties of many different software artifacts. In this paper, we present an efficient solution to verify software models which formally specified by layered graph transformation systems - special types of graph transformation systems - using a model checker called Bogor