What did you dream you would be when you were younger?
As a young child I questioned everything, and loved arguing. I adored taking things apart and seeing how they worked, even people. I also loved building things. I started out with legos, paper airplanes, model rockets, etc and eventually moved onto cars. During my teens I worked rebuilding 60's era Volkswagens. If someone had asked what I planned to do with my life at age seventeen, I would have said I wanted a workshop where I could build things.
Why did you become a researcher and how did you go about becoming a one?
In a sense I’ve always behaved as one. I went to a state-run secondary school in the mountains of Colorado (Jefferson County Open School) where students did not receive grades and they did not attend classes. Instead they set their own direction around the idea of individual projects in the context of 6 themed areas. For example my “practical skills” project was the Volkswagen rebuilding. As a part of my “adventure” project a friend and I drove to Mexico for a couple of months. I worked at a book publishing for 6 months as my “career exploration” project. There was some formal framework from which to set your goals, but largely you set your own direction. Individual or collaborative projects were proposed, executed, and then completed. The school was run by the students (from governance to the lunch programme). I went to a similar university, called The Evergreen State College. There I became obsessed with logic, mathematics, and computer programming. A professor at the university encouraged me to apply for a PhD, I did, and from there the progression was natural. Now I am at MSR, but it feels essentially like it did when I was in secondary school.
What's it like working at Microsoft Research and what do you do?
It's heaven. I have been given this unbelievable opportunity to pursue my intellectual passions, with essentially no roadblocks standing in my way. Once or twice each week I smile and laugh when I think about how amazing my position is. At MSR we have incredible flexibility, collaboration opportunities, and buildings full of the brightest people in the world. It’s a very rich environment for great breakthroughs. Frequent visits by developers and outside researchers and students also keep the environment very lively.
In terms of my technical work: I am interested in developing methods for automating reasoning and deduction, with applications in establishing the absence of bugs in critical pieces of hardware and software. For hundreds of years mathematicians and logicians have dreamt of automatic machines that proved theorems and found solutions to large and tricky puzzles. In the past 5 to 10 years we’ve seen these dreams really become a reality. I have been very fortunate to have discovered some strategies that allow us to solve problems that could not be solved before. I am perhaps best known for my work on TERMINATOR, which is used to automatically prove or disprove termination of programs and other systems (or in some cases say “I don’t know”, since this is the halting problem after all). Before TERMINATOR I worked on a tool called SLAM, which automatically proves a large class of properties called “safety properties” of programs. These tools both work within the Windows Static Driver Verifier product, which is used to validate the correctness of Windows device drivers. Techniques from these tools are also being used elsewhere, e.g. in the analysis of models of genetic regulatory pathways used by researchers in biology and the pharmaceutical industry.
What are your aspirations within your role?
I have two primary aspirations: a) mind-blowing scientific discovery, and b) the creation of opportunities for others, especially junior researchers or those considering it as a potential career path.
How has working at Microsoft Research affected your career/research goals?
MSR is like a high-performance race car: it can get you there very fast, but you have to be brave and you have to know how to drive.
Tell us an unusual/interesting fact about yourself?
I left school at age 13. The pace was so slow and there were so many rigid rules that I simply refused to go one day and that was it. So, I guess I’m a dropout. I eventually went back to school several years later when I went to the high school I mentioned before.