Model Checking Java Using Pushdown Systems
Jan Óbdržálek · 2002
In recent years, model checking algorithms for the veri cation of in nite-state systems were introduced. We evaluate the possibility of using the algorithms for pushdown systems and various modal logics of [3] for veri cation of Java programs. It turns out that pushdown systems are particularly suitable for modeling the control ow of sequential Java programs, including exceptions (which are too often not supported by model checking tools). The process of mechanical abstract model generation is described, with emphasis on supporting Java exception handling mechanism, which is the major new contribution of this paper. We also show some possible uses of our approach and present a survey of the related work.