Dr.Byron Cook is a
researcher at Microsoft's laboratory at Cambridge University. His research
interests include topics in program verification, theorem proving, and
programming languages. In recent years Dr. Cook has been working on program
termination, shape analysis, and software model checking. Dr. Cook is one
of the developers behind the Windows products called Static Driver Verifier,
which attempts to automatically prove the correctness of Windows OS device
drivers with respect to a fixed set of safety properties. Before joining
Microsoft, Dr. Cook worked at Prover Technology, where he investigated new
algorithms for use in SAT solvers and symbolic model checking tools. Dr.
Cook's PhD is from OGI
Appointments: dcm@cs.cmu.edu