Home » forums » LtU Forum

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?

By JamesLitsios at 2005-10-10 14:47 | LtU Forum | previous forum topic | next forum topic | other blogs | 2833 reads

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?

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

Microsoft

I'm not sure which domain/s you're talking about "business really being done" in. If you're talking about database-applications-in-Java business, then I wouldn't expect to see much formal methods.

On the other hand, I recall reading about Microsoft using formal methods in the context of Windows device drivers, which might interest you: Google Scholar for "Microsoft SLAM formal methods". Also, we can't forget the usual examples of failures that formal methods would have (hopefully) caught in support of your experience, but most of the big/common ones are few years ago: the priority inversion bug on that NASA probe/rover, the Therac 25 machine, etc.

By Thomas Sutton at Wed, 2005-10-12 02:34 | 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