Notice: I’ve moved my site to http://csrdu.org/nauman. You may be able to find an updated version of this page here.
My research work is aimed at formal verification of security protocols and frameworks. I’m currently working with Higher Order Logic, Isabelle (theorem prover), Z Notation, ZETA and other tools that fall in this domain. This page is currently about the learning process that I’m following. Eventually, inshaallah, it should have material related to my research work.
Articles
Update: I no longer work actively on Isabelle or Z but I still keep in touch.
April 3, 2008 at 5:00 pm
Well Z is good but is complex but those who have stuied AI n tht from Sir Nouman can understand Z very very well lol lol
September 17, 2008 at 12:55 am
Hi,
I am beginning my research in formal methods and trying to get familiar by at least one notation. I started with Z, but it is not as intuitive as I expected.
I would appreciate recommendation of a notation based on your experience.
Thanks and best of luck!
September 17, 2008 at 3:23 am
Iman, I don’t know how much experience you have but I would suggest, in general, that you get comfortable with Set Theory. It’s the basis of all formal notation and if you’re not comfortable with it from the beginning, you’ll have to learn everything from scratch.
Specifically, get to know the zermelo fraenkel theory and the way it’s formalized including the axioms and rules. There’s this book called “How to Prove It”. If you haven’t seen it, I suggest you give it a look. It’s very nice.
If you’re looking for a good tool, I would suggest Isabelle Theorem Prover but beware, it’s not easy. The learning curve is extremely steep and it takes a huge amount of time just to be able to prove simple theorems. You can get lots of help from the mailing list though.
In case you’re just trying to learn to read the notation and understand them, Z-F set theory should be enough for you.
September 17, 2008 at 3:40 am
Thanks a lot for your response. I will look at the resources you suggests.
Salam