Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. He is known for his work on programming methods and program verification tools, and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.
Prior to Microsoft Research, Leino worked at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. Leino collects thinking puzzles on a popular web page and hosts the Verification Corner channel on youtube. In his spare time, he plays music and, recently having ended his tenure as cardio exercise class instructor, is trying to learn to dance.
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.