End of Google Summer of Code - Concluding Remarks

Since the program is officially ending, everyone should know the state of the jpf-prism code at this end. In case there is anyone reading this blog that I don't email updates to, I'm going post some concluding remarks here, taken from an email I sent to my advisers/supervisors.

All the code for the project is found at the BitBucket repository, https://bitbucket.org/jpfprism/jpf-prism, which is still private, but hopefully we'll open it up soon. The Javadoc for the code, which unfortunately cannot be hosted on the same page, is located on my department webpage: http://www.math.uvic.ca/~jgorzny/jpf-prism-doc/ (and is included in the repository). A pointer to this link, as well as brief tutorials on how to install the code, run the code, and specify properties to check, can be found on the wiki on the BitBucket repository: https://bitbucket.org/jpfprism/jpf-prism/wiki/Home. 

As for the final state of the code in terms of functionality, I think it went pretty well (though not everyone was finished, I'm afraid). The short of it is that we can check any Java program that uses probabilistic functions based on Java's Random() (or jpf-probabilistic's Choice()) method. By "check" I mean that PRISM will be invoked on the states of the system and compute the probability of reaching a state with that property being true. Further, in case verification takes too long, or to confirm results, jpf-prism can be used to run the Java code repeatedly without interference, to get an empirical measure of the probability of reaching such a state. Further, the code will optimize the states of the systems if possible: it will reduce chains of states that are connected with probability 1 to a single state, unless it cannot (e.g., a choice was made, or a property must be evaluated in one, but not all of the chain's states).

So I think the project was mostly a success: the basic goal of leveraging the ease of checking a Java program with JPF and the support of probabilistic programs of PRISM has been accomplished. 

Finally, if you play around with any of the code, and something goes wrong, please let me know! I'd like to think I've got a pretty stable version of the code in the end, but if you find a bug I will be more than happy to fix it.