And in other news: JPF Workshop Day one

[purplecat]

Things I learned today

• The reason our code model checks sooo slowly, despite having a relatively conservative number of states, is that JPF (Java Pathfinder - a model checker) has an exponential slowdown based on the number of objects in the program. Our program has a lot of objects.


• Fortunately the JPF developers intend to fix this by the end of the month when no less than 10 Google Summer of Code students start work on JPF related projects.


• There is a funky looking search guidance script language we may be able to use, or failing that, base our own version on.


• When our program loops the model checker should detect this. The fact it does not is suspicious. People who know more about this than I do are now prepared to look at my code and watch this non-loop-detecting behaviour in action.


• If I'm lucky they will also explain about "Choice Generators".


• If I'm really lucky I may understand the explanation.


• Interesting things about simulating all the non-Java bits of your web application in Java so you can model check them with JPF.


• Although I understand, in principle, that people exist who have never heard of a wireless network I was quite surprised to find one working the reception desk at the Fujitsu Campus in Silicon Valley.