I am a principal researcher in the Programming
Languages and Methods group
at Microsoft Research. My research interests include a focus on
programming tools, both mental and mechanical. I lead the
Spec# project,
which explores enforceable contracts in object-oriented programming. The Spec#
language adds specifications to the object-oriented language C#, the specifications are
checked dynamically through compiler-inserted run-time checks and can be checked
statically using the automatic program verifier Boogie. We are also
starting a project to statically verify C code.Before joining Microsoft Research, I was a researcher at the Compaq Systems Research Center (Compaq SRC, formerly DEC SRC) for 7 years. Among other things at SRC, I led the Extended Static Checking for Java project (ESC/Java), which developed a precise programming tool to help programmers write and maintain programs. Before entering graduate school at Caltech, I was a technical lead in the Windows NT group at Microsoft. I hold a PhD and MS in computer science from Caltech and a BA with special honors in computer science from UT Austin.
Here is my curriculum vitae.
Here is a rebus to help you say my name (pictures by Klas Leino).
Stress the first syllable of each name. Never mind the fact that "t" appears twice in the rebus.
Some
people are surprised, even confused, by the structure of my name. But it's really quite simple:
I have 3 given names (with initials K.R.M.) and 1 family name (Leino),
where the middle one (Rustan) of the 3 given names has been designated as the one that I go by.
That's all. Nevertheless, it has happened that my name has been listed as if I were two people.
While some friends jealously have suggested that this seems to be a great way to double my number of publications, I just find
it annoying and unprofessional. To the left is a picture that proves I am but one person. Now, please go check your BibTeX files.