3 ms·

Non sequitur. 1- Guy proves 4 Colour Theorem with software, and mathematically proves the software with another program (or something like that, it isn'

by alecco 16y ago

Non 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 article, but on the other hand they kept some of the fancy sounding concepts. It would be forgivable if it weren't a tech-oriented publication. "Deep into technology."

InclinedPlane 16y ago
Yeah... It's a shame that tech and science journalism is typically so shoddy. It isn't because of merely better testing that Windows 7 / Vista are much more stable than previous versions of Windows, there are fundamental architectural changes. On modern versions of Windows if even your video driver crashes it will be restarted and instead of a BSOD you'll just get a system tray notification.
- ComputerGuru 16y ago
  Usually. But have the driver crash several times in the space of 3-5 minutes and you'll get a BSOD.
ComputerGuru 16y ago
I assume that the same technique that he used to prove the 4 color theorem can be directly applied to testing drivers (some sort of approach to addressing the halting problem???) and therefore makes it easier to spot leaks and bugs?
neilc 16y ago
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 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 it's not too surprising that a technique developed for efficient automated theorem proving would be applicable to efficient software verification. To say that doing this is solely responsible for "banishing the BSOD" is irresponsible and misinformed in a few different ways, of course.
- alecco 16y ago
  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.
- ephermata 16y ago
  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 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/ 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.)
  - thorax 16y ago
    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.

by alecco 16y ago

InclinedPlane 16y ago

Yeah... It's a shame that tech and science journalism is typically so shoddy. It isn't because of merely better testing that Windows 7 / Vista are much more stable than previous versions of Windows, there are fundamental architectural changes. On modern versions of Windows if even your video driver crashes it will be restarted and instead of a BSOD you'll just get a system tray notification.

ComputerGuru 16y ago
Usually. But have the driver crash several times in the space of 3-5 minutes and you'll get a BSOD.

ComputerGuru 16y ago

I assume that the same technique that he used to prove the 4 color theorem can be directly applied to testing drivers (some sort of approach to addressing the halting problem???) and therefore makes it easier to spot leaks and bugs?

neilc 16y ago

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 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 it's not too surprising that a technique developed for efficient automated theorem proving would be applicable to efficient software verification. To say that doing this is solely responsible for "banishing the BSOD" is irresponsible and misinformed in a few different ways, of course.

alecco 16y ago
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.
ephermata 16y ago
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 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/ 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.)
- thorax 16y ago
  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.