Disclaimers for Harshal.

Do not read between the <br>s :) I am not thinking at all...If I were capable of "thinking" about it I would be doing a Phd which I am not :)) I am just summarising information gathered from different sources.

Yes, you are right that MS uses such products internally..lots of people do, mostly OS vendors HP/M$ (I am not sure about IBM which is an irony :)) do so for verifying protocols and third party stuff like device drivers. However, they are not as omnipresent as memory profiling, performance analysis tools etc (read as tool usage has taken off in the application development space as much) I mean I wish we had had a tool like this to catch the crazy deadlock between java threads due to some convoluted synchronization code in vS just like we had purify for settling the leaks in the native code.

Connection: smatch -- based on --> stanford checker -- worked on by --> Dawson Engler and others -- founded --> Coverity.

As far as the reason for posting about this lately is concerned, one of my colleagues is doing a Phd around the same topic (he works part-time, I envy him..but he also has a lot of money so he can afford to :) ). He sent me some links to it and I also attended a talk recently on the subject.

You are also urged to try out Rose RealTime. There is a link for an eval download on the right hand side. The product is mainly used for writing software which can be modeled as a set of nested state machines and is heavily used for developing applications for embedded real time systems. It lets you concentrate on the business logic while taking away the state machine coding from you. You code whatever goes on when states change etc. It is based on the philosphy of "Model driven development". One can debug on the model level itself e.g you can put breakpoints on the states rather than on lines of code.