Registered user since Wed 17 Jun 2015
K. Rustan M. Leino works on ways to make sure programs behave as intended, secure and functionally correct. 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. He is an ACM Fellow, an IFIP Fellow, and a recipient of the CAV Award. Leino is the author of Program Proofs (MIT Press, 2023).
Leino is a research engineer at Harmonic. Previously, he has been Senior Principal Applied Scientist at Amazon Web Services, Principal Researcher at Microsoft Research, Visiting Professor at Imperial College London, and researcher 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 hosts the Verification Corner channel on youtube. He is a multi-instrumentalist, and he has instructed group cardio and strength classes.
Contributions