leino.science
© 2020-2026, K.R.M. Leino
K. Rustan M. Leino is known for his work on programming languages and programming methods 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 has been Senior Principal Applied Scientist at Amazon Web Services, co-instructor at MIT, Principal Researcher at Microsoft Research, Visiting Professor at Imperial College London, and researcher at DEC/Compaq Systems Research Center (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, he instructed group cardio and strength classes for many years, and he likes to cook.
CAV Award (2019, jointly with Jean-Christophe Filliâtre) For the design and development of reusable intermediate verification languages which significantly simplified and accelerated the building of automated deductive verifiers.
ACM Fellow (2016) For contributions to making program verification accessible and practical.
ETAPS Test of Time Award (2025, jointly with Peter Müller) For the 2006 paper A Basis for Verifying Multi-threaded Programs.
Most Influential PLDI Paper Award (2012, jointly with Cormac Flanagan, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata) For the 2002 paper Extended Static Checking for Java.
Full CV