Understand LTL? Join us!

Here is yet another software verification competition. If you are a specialist of the verification of temporal properties and you have been regretting not to snatch that easy Xbox 360 (with Kinect!) in 2011* this is your chance to make up for it!

We have the reachability part of the problems nearly done** and we are looking for someone who can reduce (at least some of) the temporal properties in the challenge to something that can be verified with the value analysis. We expect that part to be expensive so if you know how to do it we should get together and start on this as soon as possible.

(*) I am not saying that a deep understanding of temporal properties would have helped you much in 2011 but it cannot hurt to be able to think clearly about these things

(**) No really 95%. We're almost there.