Rustan Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research. He is known for his work on programming methods and program verification tools. At Microsoft Research, he has led the Spec# project, which brings enforced pre- and post-conditions to the .NET platform, and is the architect of the Boogie program verification framework, which underlies several program verifiers for Spec#, C, and other languages. Previously, Leino led the ESC/Java project at Compaq SRC and worked on specifications on the pioneering ESC/Modula-3 project at DEC SRC.
Before getting his PhD (Caltech, 1995), Leino wrote and designed object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and has recently started the Verification Corner video show on channel9.msdn.com. In his spare time, he plays music and teaches cardio exercise classes.
For more details than you want, see 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.