TechFest – Applications of Automated Reasoning

March 2, 2005
Byron Cook | Software Engineering

Several recent and fundamental advances have greatly increased the power of automated reasoning tools. Using these advances, Microsoft developed software such as Static Driver Verifier for finding bugs in device drivers. But automated reasoning libraries can be used in contexts beyond bug-finding. Examples include configuration management, scheduling, compilation, and other mathematics-based applications. In this talk I will provide information on the automated reasoning libraries that are currently available and describe how developers can use them to solve a wide variety of problems that require reasoning. I will also outline the projects within MSR to develop automated reasoning tools.

Speaker Details

Dr. Byron Cook is researcher at Microsoft’s laboratory at Cambridge University. He is also a visiting professor at Chalmers University and at Queen Mary, University of London. Byron’s research interests include automatic formal software verification, automatic theorem proving, and programming language theory. Byron has recently been working on automatic tools for proving program termination and tools for proving properties about data structures. Byron is one of the developers behind the SLAM software model checker. SLAM is now used in a Windows product called Static Driver Verifier, which automatically finds bugs in Windows OS device drivers. Before joining Microsoft, Byron worked at Prover Technology, where he investigated new algorithms for use in SAT solvers and symbolic model checking tools. Byron’s PhD is from OGI.For more information about Dr. Cook, see http://research.microsoft.com/~bycook