Thanks for the publicity John, though, for completeness, I should mentioned that me and Jason Brown will also be authoring the thesis, and a few more people will be involved as contributors too. Also, plenty more people will be working on tools that directly or indirectly build on top of (1) and (2), including software and innovative model checking techniques, among others.
If you're free in the next couple of days, I'll still be around Edinburgh and I'd be happy to meet up!