3 ms·
You might just not be hearing about what's happening in this area. Off the top of my head, formal tools are being applied at Microsoft (slam, everest, sage, Z3
by ghettoimp 7y ago
You might just not be hearing about what's happening in this area. Off the top of my head, formal tools are being applied at Microsoft (slam, everest, sage, Z3, ...), at Amazon (AWS security), at Netflix (tla+), at numerous hardware companies (Intel, AMD), at EDA vendors like Cadence and Synopsys, in avionics (DO-178C), and of course in academia (CompCert, L4 verified kernel, ...). I'm probably missing a lot.