I have just joined Facebook. It looks like a much cleaner community than Orkut. I’ve found a new group about Isabelle there and have sent you guys an invitation. Join up if you feel like it. It can be a good resource for the future and for bringing together a nice group of researchers. http://www.facebook.com/group.php?gid=18553699736
Archive by category 'Isabelle'
Now, the world can know that we’re working with Isabelle. Check out Isabelle’s world map here. And Tobias Nipkow was here in Peshawar! In March. When I was working my head off trying to get to grips with Isabelle. That was a chance missed.
I have a question and I was wondering if one of you security gurus can answer it.
There’s a lemma in the “Message” theory in Isabelle. It says, “In any message, there is an upper bound N on its greatest Nonce”.
In Isabelle:
lemma “Ex N. !!n. N <=n –>...
I’ve started working with the development of framework for protocol verification part of my Isabelle related work. Currently, this is simply copying of the Messages, Events and Public-key portion provided with Isabelle. This is mostly for my understanding. It’s already developed and many...
Alright. After much waiting and detours, I’ve finally decided to start doing some original work in Isabelle/HOL itself. *drum rolls*
After the last meeting with Mr. MM, I’ve decided to start working on the specification I’ve already done in Z of his framework. The specification is pretty...
Instructions posted on: http://recluze.wordpress.com/2007/06/17/installing-and-configuring-hol-ocl/