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?

Do a web search for

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

By raould at Mon, 2005-10-10 18:51 | login or register to post comments

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... :-)

By Josef Svenningsson at Wed, 2005-10-12 22:18 | login or register to post comments

Also

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

By Koray Can at Wed, 2005-10-12 16:32 | login or register to post comments

CUFP: Commercial Users of Functional Programming

Here is a recent workshop on the subject:
http://www.galois.com/cufp/

By JamesLitsios at Tue, 2005-10-18 07:45 | login or register to post comments

Lambda the Ultimate

User login

Navigation