?

Log in

No account? Create an account
 
 
01 May 2008 @ 07:33 pm
And in other news: JPF Workshop Day one  
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.