|
This is the Jeck Java Finite Modeling Package
It translates Java programs into a format which is understood by a hardcore symbolic modeling package called Spin, which then does lots of magic. Combined they can verify concurrency properties of simple java programs.
The source code is releseasd under the GPL and is essentially a patch on the Kopi Java Compiler
Unfortunately my amazing and highly rigorous backup procedure seems to have failed on the date that i completed programming of my project (some time in early 2000) so this version is probably from a day or so before that and probably has some critical bugs in it. ... I'll endeavour to find the working version, or failing that hack this one to a working state and maybe forward-port it to the current version of KJC.
You will also need spin : http://netlib.bell-labs.com/netlib/spin/whatispin.html
For more information read the README file
A copy of the final report abstract (gzipped postscript) and final report
If it breaks (and it probably will) try and fix it, or contact me : Owen Cliffe <occ@cs.bath.ac.uk>
6/11/2001