K. Rustan M. Leino

Registered user since Wed 17 Jun 2015

Name:K. Rustan M. Leino

K. Rustan M. Leino is Senior Principal Applied Scientist 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
Personal website:http://leino.science
Research interests:Verification, programming languages, formal methods


POPL 2022 Keynote Speaker of Tutorial 2: some advanced features of the Dafny verification tool within the Virtual Workshop-track
PLDI 2021 Speaker of Ask Me Anything with Rustan Leino within the Ask Me Anything-track
TyDe 2018 Speaker of Extrinsic vs Intrinsic Specifications, and Subset Types within the TyDe 2018-track
CPP 2018 Session Chair of Verified Applications (part of CPP 2018)
Committee Member in Program Committee within the CPP 2018-track
PLMW 2018 Author of Dafny Overview within the PLMW-track
Committee Member in Speakers within the PLMW-track
VMCAI 2018 Session Chair of Synthesis (part of VMCAI 2018)
VMCAI Session 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 2015 Author of Automatic Verification of Dafny Programs with Traits within the FTfJP-track
Committee Member in Steering Committee within the FTfJP-track
SPLASH 2012 Author of Program extrapolation with jennisys within the OOPSLA Research Papers-track
Author of Staged program development within the Keynotes-track