Automatized Data Abstraction

Model checking belongs to one of the most favourite techniques for verification of software systems. During the verification process of model checking, the whole state space of the given system is traversed. However, the state space of software systems can be huge and thus it is not possible to traverse it in reasonable amount of time. This problem is called "state explosion problem" and it can be solved using a method of abstraction that creates an abstract program from the concrete one by mapping the concrete data to abstract data. The abstract program covers all the behavior of the concrete program that is necessary for verification, but has significantly smaller state space which allows its verification in reasonable amount of time. This work is concerned in automatized data abstraction. Three known methods for automatized data abstraction are described and compared to each other. Based on these methods a new method for automatized data abstraction of object oriented programs is designed