4 ms·

Microsoft's take on making C and C++ safer - SAL: http://blogs.msdn.com/b/michael_howard/archive/2006/05/19/602077.aspx http://blogs.msdn.com/b/michael_howard/a

• profquail 15y ago
  They also created VCC (Verifying C Compiler), which uses their Z3 theorem prover to check for bugs (especially concurrency bugs, which can be really tough to find). http://vcc.codeplex.com/ http://vcc.codeplex.com/
• pascal_cuoq 15y ago
  SAL and VCC are for making C programs correct. This is related but not the same thing as making the C compiler correct. These source-level tools assume that the compiler translates the programs correctly.
  • keithnoizu 15y ago
    Hopefully we are self hosting at this point and smart enough to apply SAL and VCC to our compiler itself.