3 ms·

why those approaches never picked up outside of some academia projects?..

• Yoric 4y ago
  These days, Microsoft requires model-checking proofs before accepting new device drivers. That's their secret weapon that finally got (mostly) rid of the BSOD. I suspect that Apple is also using model-checking at various layers, but I have no proof :)
  • riku_iki 4y ago
    and how does it work? Do they write drivers in some verifiable subset of C?
    • Yoric 4y ago
      That's how I understand it. I haven't checked the details.