01SLAM and Static Driver Verifier: Model Checking Real Systems CodeMicrosoft's SLAM project brought software model checking to Windows device drivers, using counterexample-guided refinement to verify API usage rules in real C systems code.↗