K. Rustan M. Leino

Registered user since Wed 17 Jun 2015

Name: K. Rustan M. Leino

Bio: K. Rustan M. Leino is Senior Principal Engineer in the Automated Reasoning Group at Amazon Web Services. He works on ways to make sure programs behave as intended, secure and functionally correct. Leino 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.

Before Amazon, Leino has been 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, he instructed group cardio and strength classes for many years, and he likes to cook.

Country: United States

Affiliation: Amazon

Research interests: Verification, programming languages, formal methods

Contributions

TyDe 2018Speaker of Extrinsic vs Intrinsic Specifications, and Subset Types within the TyDe 2018-track
PLMW 2018Author of Dafny Overview within the PLMW-track
Committee Member in Speakers within the PLMW-track
VMCAI 2018Session Chair of Synthesis (part of VMCAI 2018)
CPP 2018Session Chair of Verified Applications (part of CPP 2018)
Committee Member in Program Committee within the CPP 2018-track
VMCAISession Chair of Welcome (part of VMCAI)
Co-chair in Program Committee
Committee Member in Program Chairs
Co-chair in Organizing Committee
Session Chair of Invited Talk II (part of VMCAI)
FTfJP 2015Author of Automatic Verification of Dafny Programs with Traits within the FTfJP-track
Committee Member in Steering Committee within the FTfJP-track
SPLASH 2012Author of Program extrapolation with jennisys within the OOPSLA Research Papers-track
Author of Staged program development within the Keynotes-track