Byron Cook

Dr. Byron Cook is researcher at Microsoft's laboratory at Cambridge University. Dr. Cook is known for his research on automating the search for program termination proofs (TERMINATOR), automatic tools for proving properties of programs that make non-trivial use of the heap (SLAyer), and automatic tools for proving safety properties of software systems (SLAM).

Dr. Cook is one of the developers behind the Windows product Static Driver Verifier, which attempts to automatically prove the correctness of Windows OS device drivers with respect to a fixed set of safety properties. For more information, see http://research.microsoft.com/~bycook.