Very interesting work with the Four Color Theorum, but the BSOD isn't exactly "banished", at least for me.
Indeed. I had a BSOD just the other day (in Vista).
How Microsoft Research banished the BSOD
11–20 of 20 posts
Re: How Microsoft Research banished the BSOD
#12Non sequitur. 1- Guy proves 4 Colour Theorem with software, and mathematically proves the software with another program (or something like that, it isn't completely clear.) 2- Most BSODs caused by 3rd party drivers. 3- Make software to test those drivers before shipping. 4- BSODs mostly gone! The article's title promised an explanation but instead they gave a flawed story. It seems on one hand they dumbed down the ar…
Well, no, they do say a little more than that: "... the techniques that George used to prove that his computer based proof was correct happens to have direct application to a set of tools that we give to people that build PC peripherals..." I know MS uses Prefast ( http://msdn.microsoft.com/en-us/library/ms933794.aspx ) to improve driver quality. I'm not sure what other verification/analysis techniques they use, but…
Perhaps I should've been more clear on that link claim on my comment. They say there's a connection but they don't even hint how both concepts are related. Not even a bad metaphor.
Re: How Microsoft Research banished the BSOD
#13I don't care how uncool Microsoft is perceived to be, Microsoft Research would be my dream job over any other tech company. It's like being a researcher at a top university without having to beg for grants every year.
I don't know. I have worked with and around academics a few times. They can be surprisingly disorganized and crisis-driven/reactive. "Gets things done" is not exactly how I would describe the academics I've encountered.
Re: How Microsoft Research banished the BSOD
#14Non sequitur. 1- Guy proves 4 Colour Theorem with software, and mathematically proves the software with another program (or something like that, it isn't completely clear.) 2- Most BSODs caused by 3rd party drivers. 3- Make software to test those drivers before shipping. 4- BSODs mostly gone! The article's title promised an explanation but instead they gave a flawed story. It seems on one hand they dumbed down the ar…
Well, no, they do say a little more than that: "... the techniques that George used to prove that his computer based proof was correct happens to have direct application to a set of tools that we give to people that build PC peripherals..." I know MS uses Prefast ( http://msdn.microsoft.com/en-us/library/ms933794.aspx ) to improve driver quality. I'm not sure what other verification/analysis techniques they use, but…
In addition to Prefast, there is also the Static Driver Verifier(SDV). Comes with the Windows Driver Kit, analyzes your code to detect common problems people have when writing drivers. The Windows Driver Kit is free -- you can learn more about SDV here:
http://www.microsoft.com/whdc/devtools/tools/sdv.mspx
SDV began its life as a project called SLAM. This page has documentation on SLAM, academic papers, etc. http://research.microsoft.com/en-us/projects/slam/
I'm not sure of the exact connection highlighted in the article, but this work builds on decades of work in automated theorem proving. It's exciting that now these techniques are used on real code.
(Disclosure: the SLAM & SDV authors are colleagues of mine at Microsoft.)
Re: How Microsoft Research banished the BSOD
#15Haha, so Microsoft decides against banishing the BSOD? So far as I know, it seems that most stuffs started at Microsoft Research end there. Therefore: good job, researcher, now I will come back to my trusted fedora. I mean, Fedora.
Re: How Microsoft Research banished the BSOD
#16Very interesting work with the Four Color Theorum, but the BSOD isn't exactly "banished", at least for me.
I haven't encountered a BSOD anywhere in all the machines I work on in at least 5 years. But I did skip Vista entirely. 64 bit Windows 7 seems mostly excellent stability wise, although I could list a few exceptions to this (Super (video converter) seemed to bring down my internet connection yesterday until I killed it), and I could make a huge list of usability gripes with it that I can't for the life of me figure out why MS doesn't fix.
But generally speaking I'm pretty happy.
Re: How Microsoft Research banished the BSOD
#17Earlier quoted context omitted.
Well, no, they do say a little more than that: "... the techniques that George used to prove that his computer based proof was correct happens to have direct application to a set of tools that we give to people that build PC peripherals..." I know MS uses Prefast ( http://msdn.microsoft.com/en-us/library/ms933794.aspx ) to improve driver quality. I'm not sure what other verification/analysis techniques they use, but…
In addition to Prefast, there is also the Static Driver Verifier(SDV). Comes with the Windows Driver Kit, analyzes your code to detect common problems people have when writing drivers. The Windows Driver Kit is free -- you can learn more about SDV here: http://www.microsoft.com/whdc/devtools/tools/sdv.mspx SDV began its life as a project called SLAM. This page has documentation on SLAM, academic papers, etc. http://r…
Also the WHQL driver verification/certification process which does additional testing internally at MS and allows you to actually install drivers without major warnings on x64/modern Windows.
Re: How Microsoft Research banished the BSOD
#18I don't care how uncool Microsoft is perceived to be, Microsoft Research would be my dream job over any other tech company. It's like being a researcher at a top university without having to beg for grants every year.
I don't know. I have worked with and around academics a few times. They can be surprisingly disorganized and crisis-driven/reactive. "Gets things done" is not exactly how I would describe the academics I've encountered.
I am curious why he is being down-voted. I am sure people disagree with him, but I'd like to at least hear some anecdotes.
Re: How Microsoft Research banished the BSOD
#19Earlier quoted context omitted.
I don't know. I have worked with and around academics a few times. They can be surprisingly disorganized and crisis-driven/reactive. "Gets things done" is not exactly how I would describe the academics I've encountered.
I am curious why he is being down-voted. I am sure people disagree with him, but I'd like to at least hear some anecdotes.
So would I. Some anecdotes about his interactions with MSR researchers would have been nice instead of seemingly random dissing of academics.
Re: How Microsoft Research banished the BSOD
#20Earlier quoted context omitted.
I am curious why he is being down-voted. I am sure people disagree with him, but I'd like to at least hear some anecdotes.
So would I. Some anecdotes about his interactions with MSR researchers would have been nice instead of seemingly random dissing of academics.
Here's one MSR employee who impresses me: http://en.wikipedia.org/wiki/Simon_Peyton_Jones