Proving that Software eventually does something good
Bio: Dr. Byron Cook is researcher at Microsoft's laboratory at Cambridge University. His research interests include topics in program verification, theorem proving, and programming languages. In recent years Byron has been working on program termination, shape analysis, and software model checking. Byron 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, Byron 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.