An algorithm and case study for the object oriented abstraction

Jakub Ratajczak


Model checking of software systems becomes more effective each day. However it still can not handle huge state spaces of real software. Particularly, concurrent systems are hard to verify. Abstraction techniques are one of the solutions aimed at managing the complexity problem. This paper describes the object oriented abstraction algorithm. It allows semi-automatic abstraction of real (i.e. Java) programs. A novelty method for constructing class abstractions is shown. It uses additional program annotations expressed in a formal manner. Proposed techniques are shown in a context of algorithms used in the Bandera toolset. A short case study of this approach is also shown.

Full Text:


Data publikacji: 2015-01-04 00:00:00
Data złożenia artykułu: 2016-04-27 10:11:09


Total abstract view - 173
Downloads (from 2020-06-17) - PDF - 0



  • There are currently no refbacks.

Copyright (c) 2015 Annales UMCS Sectio AI Informatica

Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.