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).
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.
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).
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.
Microsoft Visual Haskell when?
For a long time Microsoft employed the core team of people that developed ghc. I think Simon Marlow left a few years back, though.
Another paper on this that might have some other info.