3 ms·
I am not aware of Coq being used in the real world, but I have been told that Microsoft is using a similar tool in key parts of the Windows kernel (and that doi
by betterunix 13y ago
I am not aware of Coq being used in the real world, but I have been told that Microsoft is using a similar tool in key parts of the Windows kernel (and that doing so has drastically reduced the number of BSODs people are seeing). There is also this company, though they are not using Coq per se:
https://en.wikipedia.org/wiki/Altran_Praxis https://en.wikipedia.org/wiki/Altran_Praxis
- octo_t 13y agoMicrosofts driver development tool uses something called SLAM[1] to verify device drivers (which are the primary cause of system crashes), which uses Z3 as an SMT[2] solver. SLAM basically models the NT kernel and the Win32 API and checks for loads of bugs. [1] http://msdn.microsoft.com/en-us/library/windows/hardware/gg487498.aspx http://msdn.microsoft.com/en-us/library/windows/hardware/gg4... [2] Satisfiability Modulo Theories
- marshray 13y agoStatic Driver Verifier, one of the early flagship projects for F#! http://blogs.msdn.com/b/dsyme/archive/2007/09/19/f-ocaml-job-at-microsoft-static-driver-verifier-and-prefast-for-drivers.aspx?Redirected=true http://blogs.msdn.com/b/dsyme/archive/2007/09/19/f-ocaml-job... http://msdn.microsoft.com/en-us/library/ff552808.aspx http://msdn.microsoft.com/en-us/library/ff552808.aspx