1. 7

  2. 4

    I’ve been keeping track of the formal methods products specifically coming from Microsoft. We’re up to… 9 now? 10 if you count GHC (which is a stretch for many reasons).

    1. 4

      I lost track if you count the techniques that could be used in automation-focused tooling. Microsoft Research is simply badass. They also stay pretty close to practical focus even with high assurance stuff. Much of the work was about drivers, static analysis of C code, contracts for C# code, better compilers, and recently verified components for TLS. Their driver analyzer, SLAM, was one of most successful uses of formal methods in history in terms of boosting software reliability. I barely remember what the blue screen looks like it’s been so long.

      1. 1

        if you count GHC (which is a stretch for many reasons).

        Microsoft Visual Haskell when?

        1. 1

          For a long time Microsoft employed the core team of people that developed ghc. I think Simon Marlow left a few years back, though.

      2. 2

        Another paper on this that might have some other info.