Thanks for taking the time to provide your point of view. My initial comment was harsher than it should have been. I have no excuse, but if I had one, it would

Thanks for taking the time to provide your point of view. My initial comment was harsher than it should have been. I have no excuse, but if I had one, it would be that I see many academics in the field of formal methods act and speak as if these were used everywhere they could be useful, which is vexing when one's job is precisely of doing what is necessary to transfer them. The Z notation / B method community is still strong (though they seem a bit defensive when met at conferences). I only know about VDM because some of the syntax in Caveat is inspired from it (Caveat is the tool whose application is described in the link I provided. It was developed at the lab I work at, but before I was hired). Just in case, here is what we are now working on. One description is "successor to Caveat", but it's more than that. For one thing, it's Open Source (type "apt-get frama-c" or equivalent in most Linux distributions). It allows to combine techniques that range from static analysis to formal verification of functional properties using Hoare logic: http://frama-c.com/try_out.html http://frama-c.com/try_out.html (automatic analyses) http://frama-c.com/jessie/jessie-tutorial.pdf http://frama-c.com/jessie/jessie-tutorial.pdf (verification based on Hoare logic)