Bergen Language Design Laboratory (BLDL)

Prof. Dr. K. Rustan M. Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research and a Visiting Professor in the Computing Department at Imperial College London. He is known for his work on programming methods, languages, and verification, and is a world leader in building automated program verification tools. Languages and tools he has worked on include Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3. In the past, he has worked as a researcher at DEC and Compaq, and as a software engineer at Microsoft. He received his PhD in Computer Science from Caltech in 1995.

Leino also collects thinking puzzles on a popular web page and hosts the Verification Corner channel on youtube. In his spare time, he enjoys playing music, cooking food, cardio workouts, and dancing.

Presentation Making program verification work