Formal methods used in developing "profitable" software

I see the cryptographic community making proofs on code they write. I see static analysis used to validate certain properties of "simplified" C in "real" embeded systems but how much business is really done that uses formal methods to support their development.

Now the reason I mention this, and this is not new, that there has always been a chasm between the "academic" understanding of using mathematically oriented ideas to do things with software and the real life of hiring a developer to get a project done.
I was wondering if this community felt that things were improving.

My personal experience is not good but I will admit that looking at others I am feeling a bit more up-beat these days. Any one want to share their thoughts?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Do a web search for

The company called Praxis, might fall under what you are describing?

More Microsoft

It seems that Microsoft really wants to make an effort in shaking out bugs in their new Windows Vista. This email suggest that they are looking doing some serious analysis of their code. If Microsoft manages to pull this off and then release it to developers it might be a very important step forward for formal methods in programming.

(Gee, I never thought I'd sound so positive towards Microsoft... :-)


In case you are interested, this page describes how they used formal methods to verify an AMD processor's FP unit.

CUFP: Commercial Users of Functional Programming

Here is a recent workshop on the subject: