[Javapathfinder-user] Model checking infinitely recursive programs in JPF

[Samuel B. <sam...@gm...>]

Hello,

I am a PhD student at Brazil and am currently using JPF on my doctoral work.

I have a question about JPF: do you know any resource on JPF that allows
model checking infinitely recursive programs? Theoretically the
verification of these programs would never finish, but wouldn't it be
possible to model check them in a finite time?

Ex:
















*import gov.nasa.jpf.vm.Verify;public class ProcessVerify {    public
static void infiniterec () {        int inf = Verify.getInt(0, 1);
System.out.println ("inf == " + inf);        infiniterec2 ();    }
public static void infiniterec2 () {        int inf2 = Verify.getInt(0,
1);        System.out.println ("inf2 == " + inf2);        infiniterec
();    }    public static void main (String [] args) {
infiniterec();    }}*

How could we model check the previous program in a finite time? Do you know
how to do that?

Best,