Formal Methods

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

  1. HOLZ and Zeta
  2. ZETA Presentation

Update: I no longer work actively on Isabelle or Z but I still keep in touch.

4 Comments

  1. 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

  2. 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!

  3. 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.

  4. Thanks a lot for your response. I will look at the resources you suggests.

    Salam

Leave a Reply

Your email address will not be published.

*

© 2017 recluze

Theme by Anders NorénUp ↑