Fifth meeting of the Formal Methods Reading Group

Chapter 3 was concluded by me and Dr. Venkatesh began discussing the concept of concurrency in Chapter 4. My notes of the part of my lecture are here as FMRG-5. Dr. Venkatesh will also put up his notes soon at the wiki of http://enhanceedu.iiit.ac.in. You may send mail to choppell@gmail.com for the login name and password that are necessary to access the wiki.

Fourth Meeting of the Formal Methods Reading Group

The fourth set of notes is up as FMRG-4. In this we study automata for which there is no start state specified and all states are considered to be accepting states. This is defined as a set together with a collection of choice maps on the set. We define the notion of a strong simulation as a choice map that carries a transition between states to a transition between sets of states. Other ideas of Milner are expressed in similar terms. Would like to know from the readers if this makes it easier to understand Milner's ideas.

Third Meeting of the Formal Methods Reading Group

The third meeting took place on 3rd March. Most of the time was spent discussing the example of the faulty vending machine given by Milner as motivation for the notion of bisimilarity. It became clear that the example needs to be discussed more fully than in the earlier meeting. Accordingly the set of notes were written up. They are available here as FMRG-3. Lesson 3 is in the form of a story: "The Case of the Faulty Vending Machine - An Allegory for Software Engineers".

Second meeting of the formal methods reading group

In the second meeting we discussed the second chapter of the book. In the notes I have posted on my web site at pi-calculus I have omitted the state space diagrams. Have made do with tables describing the state diagrams. A little patience and practice will help the reader feel comfortable with them. If the readers really miss the         diagrams,  when I find some time I will try to draw and upload them at the appropriate places.

Formal Methods Reading Group

Dr. Venkatesh Choppella and I, supported by several of our colleagues, have started a Formal Methods Reading Group. We plan to have meetings once a week to pursue a learning path. To begin with we have chosen Robin Milner's 1999 book on "Communicating and Mobile Systems: the pi-calculus". Skeletal notes of the first lecture are posted on my web site as pi-calculus-1. Comments by readers, and corrections where needed, are welcome.

TCS Excellence in Computer Science Week in Pune

Haven't posted in a while.  Been busy with my course on  Program Dynamics and preparing lectures for two workshops. Attended the TCS Excellence in Computer Science (TECS) week in Pune during Jan.3 to Jan.8. The theme this year was "Formal Methods in Software Verification, Testing, and Debugging". For details the reader may go to http://121.241.184.234:8000/tecsweek/tecsweek_home.html. Shankar Natarajan's lectures were especially exciting as also his method of lecturing.  He also drew my attention to the work of Dick Lipton. I am surprised by the following item from the wikipedia article on Richard Lipton: "De Millo, Lipton and Peris criticized  the idea of formal verification of programs and argued that Formal verifications in computer science will not play the same key role as proofs do in mathematics. Absence of continuity, the inevitability of change, and the complexity of specification of real programs will make formal verification of programs difficult to justify and manage."  How about that! All power to the mathematical proofs of mapcode! All power to further research to scale it up to industrial strength! It was a treat to hear Sir Tony Hoare speak about the importance of taking the initiative and going ahead with one's plans even if they appear to be not in step with what others are doing. A boost for Prof. Nori and me. That is exactly what we have been doing over the last few years. Interactions with Prof. Jayadev Misra and Prof. C.R.Muthukrishnan were illuminating and enlightening. At the conclusion of the programme I was given an opportunity to present mapcode ideas. The slides of the presentation have been uploaded here. The novelty of the approach received a good response from some of the younger participants especially. Looks like there is a gap in pedagogics that mapcode fills. Definitely encouraging.