Mathematical skills are absolutely necessary for every researcher, who want excel in the research domain. An example can be taken of a PhD student, asked to specify its approach mathematically. Further steps, in this area means, not only specification, but some how, advanced steps, like verification....
Isabelle/HOL tutorial download link, especially for Mr. T: http://www4.in.tum.de/~nipkow/LNCS2283/tutorial.pdf See chapter 10 for Needham Shroeder Protocol case study.
Instructions posted on: http://recluze.wordpress.com/2007/06/17/installing-and-configuring-hol-ocl/
I’ve worked with Z notation now for a complete specification and here are my thoughts regarding the experience.
Now I know why Z is losing clientelle and why software engineers are reluctant to use it in practical scenarios. It has all the problems normally associated with structural programming...
A.A. I’ve uploaded the second presentation regarding ZETA and HOL-Z: Take a look.
A.A. everyone (whoever’s left here)
I’ve almost finished the specification part of the OSL. (That’s chapter 2 in the DoCoMo document.) I’ve also created a complete (albeit simple) specification in Z and type checked it using ZETA. I’ll be uploading that pretty soon inshallah....
Please take a look: http://recluze.wordpress.com/2007/04/27/zeta-presentation/
A.A. everyone.
Nothing going on in the group scene? Isn’t anybody doing anything? Or should I say, isn’t anybody writing anything about what they’re doing?
Here’s my update on my work with Z.
I’ve almost finished the Using Z book. I’m on to the chapter that has the...

