Treffer: Model checking software using infinite-state systems

After an astounding success of formal methods (especially model checking) in verifying hardware designs, the focus of interest now shifts to the area of software verification. Re-using the existing techniques, programs are usually modeled by finite-state systems. As programs usually implicitly contain potentially infinite control and data structures, these techniques do not always apply and effectively and in straightforward way. I investigate the possibility to model and verify software using infinite-state systems. Of high interest to me is model checking for various classes of temporal logics and infinite state systems, as there are encouraging decidability results for some of these classes. Moreover the logics themselves can easily express many properties of interest. The paper gives a brief general overview of the topic, followed by an example of applying LTL model checking for pushdown systems (PDS) to Java programs.